[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

Lawrence Paulson 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"):
> dest_equals
> (?'a∷{finite,perfect_space,real_normed_vector}) 

More information about the isabelle-dev mailing list