Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 28874 883ec8ee5e6e
parent 28847 648f01ec1794
child 28965 1de908189869
child 28978 f3e37d78b4f7 
--- 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
isabelle