src/Pure/Proof/extraction.ML
changeset 13719 44fed7d0c305
parent 13714 bdd483321f4b
child 13732 f8badfef5cf2
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 16 23:01:59 2002 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 17 23:43:53 2002 +0100
     1.3 @@ -478,7 +478,7 @@
     1.4                      val args = vfs_of prop;
     1.5                      val corr_prf' = foldr forall_intr_prf (args, corr_prf);
     1.6                    in
     1.7 -                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs',
     1.8 +                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs'',
     1.9                       prf_subst_TVars tye' corr_prf')
    1.10                    end
    1.11                | Some (_, prf') => (defs', prf_subst_TVars tye' prf'))
    1.12 @@ -580,7 +580,7 @@
    1.13                                    Some (map TVar (term_tvars eqn))))) %%
    1.14                              corr_prf)))
    1.15                    in
    1.16 -                    ((s, (vs', ((t', u), corr_prf'))) :: defs',
    1.17 +                    ((s, (vs', ((t', u), corr_prf'))) :: defs'',
    1.18                       subst_TVars tye' u)
    1.19                    end
    1.20                | Some ((_, u), _) => (defs, subst_TVars tye' u))