# HG changeset patch
# User wenzelm
# Date 1532783377 -7200
# Node ID d81a5da01796d90cba832334ddf45bc2f4ed4cb0
# Parent  8a071eeddb2a08e7797159baf1b027cfd0cef6d6
unused;

diff -r 8a071eeddb2a -r d81a5da01796 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Fri Jul 27 23:04:27 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Jul 28 15:09:37 2018 +0200
@@ -19,7 +19,6 @@
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val force_value: 'a lazy -> 'a lazy
-  val trim_value: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy
   val consolidate: 'a lazy list -> 'a lazy list
@@ -116,7 +115,6 @@
 fun force x = Exn.release (force_result x);
 
 fun force_value x = if is_value x then x else value (force x);
-fun trim_value x = if is_pending x then x else force_value x;
 
 
 (* map *)