# HG changeset patch
# User wenzelm
# Date 939130516 -7200
# Node ID 81e001f143a4596269d088ea43eacba57a62ba66
# Parent  2e737ce3cdb5b97c280954f4e71b7a1c9e4e7873
replaced clear_undo by clear_undos;

diff -r 2e737ce3cdb5 -r 81e001f143a4 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 05 15:34:54 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 05 15:35:16 1999 +0200
@@ -15,7 +15,7 @@
   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
-  val clear_undo: Toplevel.transition -> Toplevel.transition
+  val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
   val kill_proof: Toplevel.transition -> Toplevel.transition
@@ -74,7 +74,7 @@
 (* history commands *)
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
-val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
+val clear_undos_theory = Toplevel.history o History.clear;
 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
 
 fun undos_proof n = Toplevel.proof (fn prf =>