# HG changeset patch
# User wenzelm
# Date 1167478406 -3600
# Node ID 2cbee05b18a10a51417b43aed4bb8c7fe5c9130c
# Parent  c1a6fad248ca4ff7e0724e38a6efdea78c76c3ce
removed obsolete 'clear_undos';

diff -r c1a6fad248ca -r 2cbee05b18a1 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 30 12:33:25 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 30 12:33:26 2006 +0100
@@ -642,10 +642,6 @@
   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
 
-val clear_undosP =
-  OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
-    (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory));
-
 val redoP =
   OuterSyntax.improper_command "redo" "redo last command" K.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
@@ -938,8 +934,8 @@
   qedP, terminal_proofP, default_proofP, immediate_proofP,
   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
-  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
-  interpretationP, interpretP,
+  cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
+  interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_commandsP, print_contextP,
   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,