diff -r de62440762b8 -r 6b8107df1c3a src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Apr 05 21:08:24 2000 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 06 13:39:49 2000 +0200 @@ -612,7 +612,7 @@ (Scan.succeed IsarCmd.init_toplevel); val welcomeP = - OuterSyntax.improper_command "welcome" "print welcome message" K.control + OuterSyntax.improper_command "welcome" "print welcome message" K.diag (Scan.succeed IsarCmd.welcome);