# HG changeset patch
# User wenzelm
# Date 927279587 -7200
# Node ID 4f859545bd92240dc2158f3956dfdd4ac5176cc0
# Parent  b7293047b0f49da08c0ce8e86f2327d68eba8fc8
adapted to History changes;

diff -r b7293047b0f4 -r 4f859545bd92 src/Pure/Isar/proof_history.ML
--- a/src/Pure/Isar/proof_history.ML	Fri May 21 11:38:57 1999 +0200
+++ b/src/Pure/Isar/proof_history.ML	Fri May 21 11:39:47 1999 +0200
@@ -9,13 +9,12 @@
 sig
   type T
   exception FAIL of string
-  val init: Proof.state -> T
+  val init: int option -> Proof.state -> T
+  val is_initial: T -> bool
   val current: T -> Proof.state
   val clear: T -> T
   val undo: T -> T
   val redo: T -> T
-  val undos: int -> T -> T
-  val redos: int -> T -> T
   val position: T -> int
   val nesting: T -> int
   val prev: T -> T
@@ -54,15 +53,13 @@
 
 (* generic history operations *)
 
-fun init st = ProofHistory (History.init (((st, Seq.empty), 0), []));
+fun init lim st = ProofHistory (History.init lim (((st, Seq.empty), 0), []));
+fun is_initial (ProofHistory prf) = History.is_initial prf;
 fun current (ProofHistory prf) = fst (fst (fst (History.current prf)));
 val clear = app History.clear;
 val undo = app History.undo;
 val redo = app History.redo;
 
-fun undos n = funpow n undo;
-fun redos n = funpow n redo;
-
 
 (* navigate *)