1.1 --- a/src/Pure/Isar/runtime.ML	Wed Jun 09 15:09:00 2010 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jun 09 16:23:00 2010 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4      val detailed = ! Output.debugging;
     1.5  
     1.6      fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
     1.7 +      | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
     1.8        | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
     1.9        | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
    1.10            exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)