# HG changeset patch
# User wenzelm
# Date 1227457556 -3600
# Node ID 883ec8ee5e6e3f64623aace2bf94bcdcedb545d0
# Parent  2058a6b0eb20b2fa850ddafb10facacd2ff1a3d9
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);

diff -r 2058a6b0eb20 -r 883ec8ee5e6e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Nov 21 18:02:19 2008 +0100
+++ b/src/Pure/thm.ML	Sun Nov 23 17:25:56 2008 +0100
@@ -1642,7 +1642,7 @@
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
     val i = serial ();
-    val future = Future.fork_background (future_result i thy sorts prop o make_result);
+    val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
     val _ = add_future thy future;
     val promise = (i, future);
   in