--- a/src/Pure/Isar/toplevel.ML Tue Jul 10 23:29:43 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jul 10 23:29:44 2007 +0200
@@ -751,9 +751,7 @@
in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
fun raw_loop src =
- let val prompt =
- Output.escape ((Markup.output Markup.prompt |-> enclose) Source.default_prompt)
- in
+ let val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt) in
(case get_interrupt (Source.set_prompt prompt src) of
NONE => (writeln "\nInterrupt."; raw_loop src)
| SOME NONE => if warn_secure () then quit () else ()