Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/toplevel.ML
changeset 28458 0966ac3f4a40
parent 28453 06702e7acd1d
child 28463 b8f16c92122a 
--- 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."
isabelle