renamed map to map_current;

--- 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;