refrain from setting ml_prompts again;
authorwenzelm
Sat, 30 Dec 2006 16:08:07 +0100
changeset 21967 dcb32fe97503
parent 21966 edab0ecfbd7c
child 21968 883cd697112e
refrain from setting ml_prompts again;
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 ();