--- a/src/Pure/proofterm.ML Thu Aug 19 12:01:57 2021 +0200
+++ b/src/Pure/proofterm.ML Thu Aug 19 12:30:20 2021 +0200
@@ -266,8 +266,6 @@
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
-val consolidate_body = consolidate_bodies o single;
-
fun make_thm_node theory_name name prop body export =
let
val consolidate =
@@ -1983,7 +1981,7 @@
fun fulfill () =
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
in
- if null promises then Future.map (postproc #> tap consolidate_body) body
+ if null promises then Future.map postproc body
else if Future.is_finished body andalso length promises = 1 then
Future.map (fn _ => fulfill ()) (snd (hd promises))
else