# HG changeset patch
# User wenzelm
# Date 1231620422 -3600
# Node ID dc6b19966757a36ee7f6b065ebc32b23798ff0dc
# Parent  a5f84ac146090aca3ee7201a01e831590c9ef255
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

diff -r a5f84ac14609 -r dc6b19966757 src/Pure/thm.ML
--- 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),