'kill' made improper;
authorwenzelm
Tue, 01 Jun 1999 19:47:10 +0200
changeset 6757 604d1445c9f3
parent 6756 fe6eb161df3e
child 6758 8fc15183f549
'kill' made improper;
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 =