# HG changeset patch
# User wenzelm
# Date 953307066 -3600
# Node ID efa136cbde2977448c7e8473e95b705e6cc4f108
# Parent  8958ece3bbdfcdbf1bb7ea05792662a06251cd1b
generic "kill" command;

diff -r 8958ece3bbdf -r efa136cbde29 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Mar 17 16:30:45 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 17 16:31:06 2000 +0100
@@ -27,10 +27,6 @@
   OuterSyntax.command "end" "end current excursion" K.thy_end
     (Scan.succeed (Toplevel.print o Toplevel.exit));
 
-val kill_excursionP =
-  OuterSyntax.improper_command "kill" "kill current excursion" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.kill));
-
 val contextP =
   OuterSyntax.improper_command "context" "switch theory context" K.thy_switch
     (P.name >> (Toplevel.print oo IsarThy.context));
@@ -460,6 +456,10 @@
   OuterSyntax.improper_command "undo" "undo last command" K.control
     (Scan.succeed (Toplevel.print o IsarCmd.undo));
 
+val killP =
+  OuterSyntax.improper_command "kill" "kill current history node" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.kill));
+
 
 
 (** diagnostic commands (for interactive mode only) **)
@@ -626,7 +626,7 @@
 
 val parsers = [
   (*theory structure*)
-  theoryP, end_excursionP, kill_excursionP, contextP,
+  theoryP, end_excursionP, contextP,
   (*markup commands*)
   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
@@ -643,7 +643,7 @@
   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
   proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
-  undos_proofP, kill_proofP, undoP,
+  undos_proofP, kill_proofP, undoP, killP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,