# HG changeset patch
# User wenzelm
# Date 1181685722 -7200
# Node ID 6e1786a6f6367ba8d3e559a569a407140853144e
# Parent  e0b5a74d7ace103dcf10ec47f0ed5c0821fc06b6
renamed map to map_current;

diff -r e0b5a74d7ace -r 6e1786a6f636 src/Pure/General/history.ML
--- a/src/Pure/General/history.ML	Wed Jun 13 00:02:01 2007 +0200
+++ b/src/Pure/General/history.ML	Wed Jun 13 00:02:02 2007 +0200
@@ -17,7 +17,7 @@
   val redo: '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
+  val map_current: ('a -> 'a) -> 'a T -> 'a T
 end;
 
 structure History: HISTORY =
@@ -55,6 +55,6 @@
 
 fun apply f hist = apply' (current hist) f hist;
 
-fun map f (History (x, hist)) = History (f x, hist);
+fun map_current f (History (x, hist)) = History (f x, hist);
 
 end;