diff -r 832ec852fc4e -r 263051aaf0de src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sun Nov 29 13:17:42 1998 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sun Nov 29 13:19:48 1998 +0100 @@ -179,7 +179,7 @@ fun main () = (Toplevel.set_state Toplevel.toplevel; ml_prompts "ML> " "ML# "; - writeln ("\n\n" ^ Context.welcome ()); + writeln (Context.welcome ()); loop ());