src/Pure/Proof/extraction.ML
changeset 13793 c02c81fd11b8
parent 13732 f8badfef5cf2
child 14472 cba7c0a3ffb3
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Jan 29 16:34:51 2003 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jan 29 17:32:01 2003 +0100
     1.3 @@ -537,7 +537,7 @@
     1.4                      val corr_prop = Reconstruct.prop_of corr_prf;
     1.5                      val corr_prf' = foldr forall_intr_prf
     1.6                        (map (get_var_type corr_prop) (vfs_of prop), proof_combt
     1.7 -                         (PThm ((corr_name name vs, []), corr_prf, corr_prop,
     1.8 +                         (PThm ((corr_name name vs', []), corr_prf, corr_prop,
     1.9                               Some (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
    1.10                    in
    1.11                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',