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