--- a/src/Pure/System/isar.ML Mon Nov 11 18:37:56 2013 +0100
+++ b/src/Pure/System/isar.ML Mon Nov 11 20:00:53 2013 +0100
@@ -97,7 +97,7 @@
| SOME (_, SOME exn_info) =>
(set_exn (SOME exn_info);
Toplevel.setmp_thread_position tr
- Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+ ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
true)
| SOME (st', NONE) =>
let
@@ -144,7 +144,7 @@
NONE => if secure then quit () else ()
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
handle exn =>
- (Output.error_msg (ML_Compiler.exn_message exn)
+ (ML_Compiler.exn_error_message exn
handle crash =>
(Synchronized.change crashes (cons crash);
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");