# HG changeset patch
# User wenzelm
# Date 1222950160 -7200
# Node ID 0966ac3f4a40a39a2a711077124c5af2d0298a5a
# Parent  25669513fd4c7abd504d0185525f5d09754759d0
simplified Exn.EXCEPTIONS;

diff -r 25669513fd4c -r 0966ac3f4a40 src/Pure/Isar/proof.ML
--- 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
diff -r 25669513fd4c -r 0966ac3f4a40 src/Pure/Isar/toplevel.ML
--- 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."