--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Jun 06 21:11:23 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Jun 06 21:11:23 2009 +0200
@@ -1000,7 +1000,7 @@
| (Toplevel.UNDEF,SOME src) =>
(Output.error_msg "No working context defined"; loop true src)
| (e,SOME src) =>
- (Output.error_msg (Toplevel.exn_message e); loop true src)
+ (Output.error_msg (ML_Compiler.exn_message e); loop true src)
| (PGIP_QUIT,_) => ()
| (_,NONE) => ()
in
--- a/src/Pure/System/isar.ML Sat Jun 06 21:11:23 2009 +0200
+++ b/src/Pure/System/isar.ML Sat Jun 06 21:11:23 2009 +0200
@@ -134,7 +134,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 (Toplevel.exn_message exn)
+ (Output.error_msg (ML_Compiler.exn_message exn)
handle crash =>
(CRITICAL (fn () => change crashes (cons crash));
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
--- a/src/Pure/System/session.ML Sat Jun 06 21:11:23 2009 +0200
+++ b/src/Pure/System/session.ML Sat Jun 06 21:11:23 2009 +0200
@@ -107,6 +107,6 @@
|> setmp_noncritical Multithreading.max_threads
(if Multithreading.available then max_threads
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
- handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
+ handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
end;