# HG changeset patch
# User wenzelm
# Date 928259230 -7200
# Node ID 604d1445c9f3a63d2375279d8e730548a30faca2
# Parent  fe6eb161df3e52625d2b82c98a74299258849bf3
'kill' made improper;

diff -r fe6eb161df3e -r 604d1445c9f3 src/Pure/Isar/isar_syn.ML
--- 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 =