[isabelle] Different behavior in Jedit and Emacs



Hi all,
we just came across  the following problem when using the datatype command. The following datatype definition works when using Jedit but does not work when using Emacs as interface. In the previous distribution the example used to work with Emacs as well.

theory test
imports Main
begin

datatype 'a tree =
           leaf "'a"
         | node "nat \<Rightarrow> 'a tree"        

datatype 'a dtype  = constr "'a tree"

end


When using Emacs, we get the following error message:

*** Proof failed.
*** dtype_size fa (constr tree) = 0
***  1. Suc 0 = 0
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** dtype_size fa (constr tree) = 0


Thanks for any suggestions!






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.