# HG changeset patch
# User wenzelm
# Date 1162664741 -3600
# Node ID 98c0405f54933b503ea9c4edb7303b0fc0a749d2
# Parent  4d733b76b5fa8abcd0573487d52a4355e7645247
replaced apply_copy by apply';
tuned;

diff -r 4d733b76b5fa -r 98c0405f5493 src/Pure/General/history.ML
--- a/src/Pure/General/history.ML	Sat Nov 04 19:25:41 2006 +0100
+++ b/src/Pure/General/history.ML	Sat Nov 04 19:25:41 2006 +0100
@@ -15,7 +15,7 @@
   val clear: int -> 'a T -> 'a T
   val undo: 'a T -> 'a T
   val redo: 'a T -> 'a T
-  val apply_copy: ('a -> 'a) -> ('a -> 'a) -> 'a T -> 'a T
+  val apply': 'a -> ('a -> 'a) -> 'a T -> 'a T
   val apply: ('a -> 'a) -> 'a T -> 'a T
   val map: ('a -> 'a) -> 'a T -> 'a T
 end;
@@ -23,9 +23,6 @@
 structure History: HISTORY =
 struct
 
-
-(* datatype history *)
-
 datatype 'a T =
   History of 'a * (int option * int * 'a list * 'a list);
 
@@ -53,13 +50,11 @@
   | push (SOME 0) _ _ _ = []
   | push (SOME n) len x xs = if len < n then x :: xs else Library.take (n, x :: xs);
 
-fun apply_copy cp f (History (x, (lim, len, undo_list, _))) =
-  let val x' = cp x
-  in History (f x, (lim, len + 1, push lim len x' undo_list, [])) end;
+fun apply' x' f (History (x, (lim, len, undo_list, _))) =
+  History (f x, (lim, len + 1, push lim len x' undo_list, []));
 
-fun apply f = apply_copy I f;
+fun apply f hist = apply' (current hist) f hist;
 
 fun map f (History (x, hist)) = History (f x, hist);
 
-
 end;