future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
authorwenzelm
Sat Jan 10 21:47:02 2009 +0100 (2009-01-10)
changeset 29436dc6b19966757
parent 29435 a5f84ac14609
child 29437 a96236886804
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Sat Jan 10 21:32:30 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Jan 10 21:47:02 2009 +0100
     1.3 @@ -1613,7 +1613,7 @@
     1.4      val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
     1.5  
     1.6      val i = serial ();
     1.7 -    val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
     1.8 +    val future = future_thm |> Future.map (future_result i thy sorts prop);
     1.9      val promise = (i, future);
    1.10    in
    1.11      Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),