--- 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'',
--- 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)) =