tuned: more parallel;

--- a/src/Pure/Concurrent/lazy.ML	Mon Feb 19 18:01:36 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Mon Feb 19 18:12:28 2018 +0100
@@ -18,7 +18,6 @@
   val is_finished: 'a lazy -> bool
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
-  val force_list: 'a lazy list -> 'a list
   val force_value: 'a lazy -> 'a lazy
   val trim_value: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
@@ -112,10 +111,6 @@
 
 fun force x = Exn.release (force_result x);
 
-fun force_list xs =
-  (List.app (fn x => if is_pending x then ignore (force_result x) else ()) xs;
-   map force xs);
-
 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;
 

--- a/src/Pure/proofterm.ML	Mon Feb 19 18:01:36 2018 +0100
+++ b/src/Pure/proofterm.ML	Mon Feb 19 18:12:28 2018 +0100
@@ -199,7 +199,7 @@
 
 val consolidate =
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
-  #> Lazy.force_list #> ignore;
+  #> Lazy.consolidate #> map Lazy.force #> ignore;
 
 fun make_thm_node name prop body =
   Thm_Node {name = name, prop = prop, body = body,