# HG changeset patch
# User wenzelm
# Date 1244315483 -7200
# Node ID 5e412e4c654614f92fe7c78b079f31c9686aed7b
# Parent  ae1a00e1a2f67a4e1bb9cb494c4761bf75669ed0
ML_Compiler.exn_message;

diff -r ae1a00e1a2f6 -r 5e412e4c6546 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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
diff -r ae1a00e1a2f6 -r 5e412e4c6546 src/Pure/System/isar.ML
--- 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");
diff -r ae1a00e1a2f6 -r 5e412e4c6546 src/Pure/System/session.ML
--- 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;