[isabelle-dev] Basic_Thm.thm

Walther Neuper wneuper at ist.tugraz.at
Mon Feb 21 13:15:05 CET 2011

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 

What is going on here ?

More information about the isabelle-dev mailing list