# HG changeset patch
# User wenzelm
# Date 1256059681 -7200
# Node ID 207c21697a48e70887f4d8bc5e59d6984a2dfa9d
# Parent  c95102496490a2176ae33aab986b47304f3e536c
removed unused map_force;

diff -r c95102496490 -r 207c21697a48 src/Pure/Concurrent/lazy.ML
--- 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;
 
diff -r c95102496490 -r 207c21697a48 src/Pure/Concurrent/lazy_sequential.ML
--- 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;