[isabelle-dev] Pending sort hypotheses

[Amine Chaieb]

Dear all,


I am having problems with updating a theory, which used to work by the
end of last year.


Now I get at some point the following error: 

Pending sort hypotheses: {ring_char_0,division_by_zero,field}


after simp has succeeded to solve the goal.


The problem is that none of by Hypotheses, assumptions or goal depend on
these sorts!!


I have tried to trace the simplifier (I had also a strange experience
here, even when I set the trace depth limit to 1000000 I still get a
broken trace at the same places with limit roughly 1000). In the over
68K lines of trace there is no mention of any type 'a with those sorts.


The proof used to by one line (by simp).


Anybody knows how to explain this behaviour?


Best wishes,

Amine.