src/Pure/Isar/isar_syn.ML
changeset 6757 604d1445c9f3
parent 6755 9f830d69a46d
child 6773 83c09a9684cf
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 01 19:46:52 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 01 19:47:10 1999 +0200
@@ -28,7 +28,7 @@
     (Scan.succeed (Toplevel.print o Toplevel.exit));
 
 val kill_excursionP =
-  OuterSyntax.command "kill" "kill current excursion" K.control
+  OuterSyntax.improper_command "kill" "kill current excursion" K.control
     (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
 
 val contextP =