author | wenzelm |
Thu, 06 Apr 2000 13:39:49 +0200 | |
changeset 8678 | 6b8107df1c3a |
parent 8677 | de62440762b8 |
child 8679 | 553ab81a5fee |
--- 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);