src/Pure/Proof/extraction.ML
changeset 30718 15041c7e51e4
parent 30528 7173bf123335
child 32032 a6a6e8031c14
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:17 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:49 2009 +0100
     1.3 @@ -568,7 +568,7 @@
     1.4                        (proof_combt
     1.5                           (PThm (serial (),
     1.6                            ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
     1.7 -                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
     1.8 +                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
     1.9                        (map (get_var_type corr_prop) (vfs_of prop))
    1.10                    in
    1.11                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
    1.12 @@ -679,7 +679,7 @@
    1.13                        (proof_combt
    1.14                          (PThm (serial (),
    1.15                           ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.16 -                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.17 +                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
    1.18                        (map (get_var_type corr_prop) (vfs_of prop));
    1.19                    in
    1.20                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',