thanks for the answer.
our problem has not been caused by Isabelle ...
On 02/21/2011 04:14 PM, Makarius wrote:
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)?
We were not able to reproduce this either with the original Isabelle2011
bundle.
This observation led to the solution:
We had library.ML from Larry in place of library.sml from ISAC. We
replaced the file and it works now.
How library.ML could cause the strange behavior is a question not yet
solved, updating ISAC to Isabelle2011 has higher priority ;-)
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
Sorry for the inconvenience
Walther
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
