future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
authorwenzelm
Sun Nov 23 17:25:56 2008 +0100 (2008-11-23)
changeset 28874883ec8ee5e6e
parent 28873 2058a6b0eb20
child 28875 c1c0e23ed063
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Nov 21 18:02:19 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Sun Nov 23 17:25:56 2008 +0100
     1.3 @@ -1642,7 +1642,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.fork_background (future_result i thy sorts prop o make_result);
     1.8 +    val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
     1.9      val _ = add_future thy future;
    1.10      val promise = (i, future);
    1.11    in