'kill' made improper;
authorwenzelm
Tue Jun 01 19:47:10 1999 +0200 (1999-06-01 ago)
changeset 6757604d1445c9f3
parent 6756 fe6eb161df3e
child 6758 8fc15183f549
'kill' made improper;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jun 01 19:46:52 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 01 19:47:10 1999 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4      (Scan.succeed (Toplevel.print o Toplevel.exit));
     1.5  
     1.6  val kill_excursionP =
     1.7 -  OuterSyntax.command "kill" "kill current excursion" K.control
     1.8 +  OuterSyntax.improper_command "kill" "kill current excursion" K.control
     1.9      (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
    1.10  
    1.11  val contextP =