removed obsolete 'clear_undos';
authorwenzelm
Sat Dec 30 12:33:26 2006 +0100 (2006-12-30)
changeset 219562cbee05b18a1
parent 21955 c1a6fad248ca
child 21957 4e44e74dc7e7
removed obsolete 'clear_undos';
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 30 12:33:25 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 30 12:33:26 2006 +0100
     1.3 @@ -642,10 +642,6 @@
     1.4    OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
     1.5      (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
     1.6  
     1.7 -val clear_undosP =
     1.8 -  OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
     1.9 -    (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory));
    1.10 -
    1.11  val redoP =
    1.12    OuterSyntax.improper_command "redo" "redo last command" K.control
    1.13      (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
    1.14 @@ -938,8 +934,8 @@
    1.15    qedP, terminal_proofP, default_proofP, immediate_proofP,
    1.16    done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
    1.17    apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.18 -  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    1.19 -  interpretationP, interpretP,
    1.20 +  cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
    1.21 +  interpretP,
    1.22    (*diagnostic commands*)
    1.23    pretty_setmarginP, helpP, print_commandsP, print_contextP,
    1.24    print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,