src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 16:08:06 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 16:08:07 2006 +0100
@@ -314,8 +314,7 @@
 
 fun gen_loop term no_pos =
  (Context.reset_context ();
-  Toplevel.loop (isar term no_pos);
-  ml_prompts "ML> " "ML# ");
+  Toplevel.loop (isar term no_pos));
 
 fun gen_main term no_pos =
  (Toplevel.init_state ();