OK, I see now that buried somewhere in Abstract_Rat old unconstrained rewrites have a new assupmtion
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" That might explain some of the bahaviour. Amine. Amine Chaieb wrote: > 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. > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >