diff -r 5f4448e60662 -r ad8ca85f13e2 src/Pure/proofterm.ML
--- 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,