# HG changeset patch
# User wenzelm
# Date 926439517 -7200
# Node ID f81b9b4c3265fe3113b1743f3051a4ce0bf1a4c5
# Parent  6f74e7aa5b4d2ca8bba38cf63e10021ff111d461
fixed msg;

diff -r 6f74e7aa5b4d -r f81b9b4c3265 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue May 11 17:51:23 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue May 11 18:18:37 1999 +0200
@@ -42,7 +42,7 @@
 
 val exit = Toplevel.keep (fn state =>
   (Context.set_context (try Toplevel.theory_of state);
-    writeln "Leaving the Isar loop.  Invoke 'main_loop();' to restart.";
+    writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
     raise Toplevel.TERMINATE));
 
 val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);