refrain from setting ml_prompts again;
authorwenzelm
Sat Dec 30 16:08:07 2006 +0100 (2006-12-30)
changeset 21967dcb32fe97503
parent 21966 edab0ecfbd7c
child 21968 883cd697112e
refrain from setting ml_prompts again;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 16:08:06 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 16:08:07 2006 +0100
     1.3 @@ -314,8 +314,7 @@
     1.4  
     1.5  fun gen_loop term no_pos =
     1.6   (Context.reset_context ();
     1.7 -  Toplevel.loop (isar term no_pos);
     1.8 -  ml_prompts "ML> " "ML# ");
     1.9 +  Toplevel.loop (isar term no_pos));
    1.10  
    1.11  fun gen_main term no_pos =
    1.12   (Toplevel.init_state ();