[isabelle-dev] Basic_Thm.thm

[Makarius]

On Mon, 21 Feb 2011, Walther Neuper wrote:

> 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 ?

This is very strange.  Are you really using Isabelle2011 here (which BTW 
would mean you can ask such questions on isabelle-users)?

Type aliases are sometimes printed differently after some change of ML 
compiler configuration, but I am not aware of anything like that at the 
moment.  With the official Isabelle2011 bundle from the Isabelle website I 
cannot reproduce any of the above problems.


 	Makarius