changeset 29436 | dc6b19966757 |
parent 29432 | 5bb5551bef03 |
child 29636 | d01bada1df33 |
--- a/src/Pure/thm.ML Sat Jan 10 21:32:30 2009 +0100 +++ b/src/Pure/thm.ML Sat Jan 10 21:47:02 2009 +0100 @@ -1613,7 +1613,7 @@ val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial (); - val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof); + val future = future_thm |> Future.map (future_result i thy sorts prop); val promise = (i, future); in Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),