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