Re: [isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks

2013-04-05 Thread Thomas Sewell
None of us reported my problem, because it concerned a somewhat elaborate case in some somewhat elaborate code I wrote, which we never managed to conveniently reproduce. Noone realised at the time that the exception-printing mechanism was at fault all by itself. This would be an archetypal bad

[isabelle-dev] auto raises a TYPE exception

2013-04-05 Thread Johannes Hölzl
Hi, In Isabelle2013 as well as the current development revision (#0a7b4e0384d0) the following call to auto raises a TYPE exception in envir.ML 8 theory Scratch imports Main begin class test = fixes P :: 'a set ⇒ bool lemma shows P_UNIV [intro]: P UNIV and P_Int [intro]: P S

Re: [isabelle-dev] auto raises a TYPE exception

2013-04-05 Thread Makarius
On Fri, 5 Apr 2013, Johannes Hölzl wrote: It looks like the problem is somewhere in the call to Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML): clasimp.ML fun nodup_depth_tac ctxt m i st = SELECT_GOAL (Classical.safe_steps_tac ctxt 1 THEN_ELSE (DEPTH_SOLVE

Re: [isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks

2013-04-05 Thread Makarius
On Fri, 5 Apr 2013, Thomas Sewell wrote: By comparison, David is providing you with what would be considered a good bug report in most open-source communities. It comes with a clear explanation not only of what the problem is but what causes it to occur, and how it might be fixed. In such