--- a/src/Pure/Isar/toplevel.ML Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jul 24 19:44:35 2007 +0200
@@ -257,7 +257,7 @@
| exn_msg _ Output.TOPLEVEL_ERROR = "Error."
| exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
| exn_msg _ (ERROR msg) = msg
- | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
+ | exn_msg detailed (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg detailed) exns @ [msg])
| exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
| exn_msg false (THEORY (msg, _)) = msg
| exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)