[isabelle-dev] Basic_Thm.thm

[Walther Neuper]

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