Isar.loop;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Nov 02 14:46:58 2005 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Nov 02 14:47:00 2005 +0100
@@ -101,7 +101,7 @@
 
 val exit = Toplevel.keep (fn state =>
   (Context.set_context (try Toplevel.theory_of state);
-    writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
+    writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
     raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;