diff -r 181bbcee76f5 -r 80dd2f5780df src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:41 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:42 2005 +0200
@@ -372,7 +372,8 @@
 
 fun gen_loop term no_pos =
  (Context.reset_context ();
-  Toplevel.loop (isar term no_pos));
+  Toplevel.loop (isar term no_pos);
+  ml_prompts "ML> " "ML# ");
 
 fun gen_main term no_pos =
  (Toplevel.set_state Toplevel.toplevel;