# HG changeset patch
# User wenzelm
# Date 1237996489 -3600
# Node ID 15041c7e51e404ce7c23cb840769ff3fb7ceb517
# Parent  465093aa58449453da9a480616d22ee9fa633f4f
Proofterm.approximate_proof_body;

diff -r 465093aa5844 -r 15041c7e51e4 src/Pure/Proof/extraction.ML
--- 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'',
diff -r 465093aa5844 -r 15041c7e51e4 src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Wed Mar 25 16:54:17 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Wed Mar 25 16:54:49 2009 +0100
@@ -158,7 +158,7 @@
   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
       (* FIXME? *)
       PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
-        Future.value (Proofterm.make_proof_body MinProof)))
+        Future.value (Proofterm.approximate_proof_body MinProof)))
   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =