[isabelle-dev] Basic_Thm.thm

[Walther Neuper]

updating from Isabelle2009-2 to Isabelle2011 I see that the type thm is 
qualified now:

     ML {* @{thm refl} *}
     val it = "?t = ?t": Basic_Thm.thm

So we change our code to for instance:

     ML {* datatype rrr = TTT of Basic_Thm.thm * int *}

     datatype rrr = TTT of thm * int

The response is dubious: thm instead of Basic_Thm.thm; and actually we get

     ML {* TTT (@{thm refl}, 0) *}

     *** Type error in function application. Function: TTT : thm * int 
-> rrr
     ***    Argument: (Isabelle.thm, 0) : Basic_Thm.thm * int
     ***    Reason: Can't unify thm with Basic_Thm.thm (Different type 
constructors)

What is going on here ?
Walther