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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
