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/Proof/extraction.ML
changeset 30718 15041c7e51e4
parent 30528 7173bf123335
child 32032 a6a6e8031c14 
--- a/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:17 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:49 2009 +0100
@@ -568,7 +568,7 @@
                       (proof_combt
                          (PThm (serial (),
                           ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
+                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop))
                   in
                     ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
@@ -679,7 +679,7 @@
                       (proof_combt
                         (PThm (serial (),
                          ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
+                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop));
                   in
                     ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
isabelle