removed unused map_force;

--- a/src/Pure/Concurrent/lazy.ML	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Tue Oct 20 19:28:01 2009 +0200
@@ -12,7 +12,6 @@
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
-  val map_force: ('a -> 'b) -> 'a lazy -> 'b lazy
 end;
 
 structure Lazy: LAZY =
@@ -49,8 +48,6 @@
 
 fun force r = Exn.release (force_result r);
 
-fun map_force f = value o f o force;
-
 end;
 end;
 

--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Tue Oct 20 19:28:01 2009 +0200
@@ -34,8 +34,6 @@
 
 fun force r = Exn.release (force_result r);
 
-fun map_force f = value o f o force;
-
 end;
 end;