[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses
lp15 at cam.ac.uk
Tue Jul 3 20:42:07 CEST 2012
This is obviously a bug.
Does anybody know (without going to the trouble of reproducing this exact proof and obtaining a backtrace) why the function dest_equals is being called on a sort constraint? At a guess, something is expecting a definition.
Begin forwarded message:
> Oh, I forgot to say that if i start the first proof with "proof (unfold_locales, auto simp:sort_constraint_def)", as suggested by Makarius, the exception still raises :
> exception TERM raised (line 137 of "more_thm.ML"):
More information about the isabelle-dev