author | wenzelm |
Tue, 17 May 2005 18:10:42 +0200 | |
changeset 15989 | 80dd2f5780df |
parent 15988 | 181bbcee76f5 |
child 15990 | 4ef32dcbb44f |
--- a/src/Pure/Isar/outer_syntax.ML Tue May 17 18:10:41 2005 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Tue May 17 18:10:42 2005 +0200 @@ -372,7 +372,8 @@ fun gen_loop term no_pos = (Context.reset_context (); - Toplevel.loop (isar term no_pos)); + Toplevel.loop (isar term no_pos); + ml_prompts "ML> " "ML# "); fun gen_main term no_pos = (Toplevel.set_state Toplevel.toplevel;