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

[Lawrence Paulson]

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.

Larry

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
> SORT_CONSTRAINT
> (?'a∷{finite,perfect_space,real_normed_vector}) 
> 
>