changeset 18063 | c4bffc47c11b |
parent 17899 | 0e0ac7700f57 |
child 18135 | 41cec935e804 |
--- 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;