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);