author | wenzelm |
Tue, 01 Jun 1999 19:47:10 +0200 | |
changeset 6757 | 604d1445c9f3 |
parent 6756 | fe6eb161df3e |
child 6758 | 8fc15183f549 |
--- 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 =