| changeset 67669 | ad8ca85f13e2 |
| parent 66168 | fcd09fc36d7f |
| child 68026 | a8ee8e4884ec |
--- 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,