tuned;
authorwenzelm
Thu Dec 15 21:16:10 2016 +0100 (2016-12-15)
changeset 6457107bbdb2079db
parent 64570 a2e7862e7dd5
child 64572 cec07f7249cd
tuned;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Dec 15 15:08:18 2016 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Dec 15 21:16:10 2016 +0100
     1.3 @@ -585,9 +585,8 @@
     1.4  and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
     1.5  
     1.6  fun fulfill_body (th as Thm (Deriv {promises, body}, _)) =
     1.7 -  Proofterm.fulfill_norm_proof (theory_of_thm th) (fulfill_promises promises) body
     1.8 -and fulfill_promises promises =
     1.9 -  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
    1.10 +  let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
    1.11 +  in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;
    1.12  
    1.13  fun proof_bodies_of thms =
    1.14    let