--- a/src/Pure/Isar/proof.ML Thu Oct 02 14:22:36 2008 +0200
+++ b/src/Pure/Isar/proof.ML Thu Oct 02 14:22:40 2008 +0200
@@ -963,7 +963,7 @@
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
| Exn.Exn Exn.Interrupt => raise Exn.Interrupt
- | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
+ | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
in
--- a/src/Pure/Isar/toplevel.ML Thu Oct 02 14:22:36 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Oct 02 14:22:40 2008 +0200
@@ -258,8 +258,7 @@
val detailed = ! debug;
fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
- | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns)
- | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg])
+ | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
| exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
| exn_msg _ TERMINATE = "Exit."