src/Pure/Isar/outer_syntax.ML
changeset 15989 80dd2f5780df
parent 15973 5fd94d84470f
child 16195 0eb3c15298cd
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:42 2005 +0200
     1.3 @@ -372,7 +372,8 @@
     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 +  Toplevel.loop (isar term no_pos);
     1.9 +  ml_prompts "ML> " "ML# ");
    1.10  
    1.11  fun gen_main term no_pos =
    1.12   (Toplevel.set_state Toplevel.toplevel;