src/Pure/Isar/isar_syn.ML
changeset 6757 604d1445c9f3
parent 6755 9f830d69a46d
child 6773 83c09a9684cf
     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 =