src/Pure/thm.ML
changeset 32810 f3466a5645fa
parent 32784 1a5dde5079ac
child 33037 b22e44496dc2
     1.1 --- a/src/Pure/thm.ML	Thu Oct 01 14:11:28 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 01 14:27:50 2009 +0200
     1.3 @@ -540,7 +540,7 @@
     1.4  fun raw_body (Thm (Deriv {body, ...}, _)) = body;
     1.5  
     1.6  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
     1.7 -  Pt.fulfill_proof (Theory.deref thy_ref) ~1
     1.8 +  Pt.fulfill_proof (Theory.deref thy_ref)
     1.9      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    1.10  and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    1.11