src/Pure/Isar/outer_syntax.ML
changeset 21967 dcb32fe97503
parent 21957 4e44e74dc7e7
child 22086 cf6019fece63
     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 ();