Fixed small bug that caused some definitions to be "forgotten".
authorberghofe
Sun Nov 17 23:43:53 2002 +0100 (2002-11-17)
changeset 1371944fed7d0c305
parent 13718 9f94248d2f5a
child 13720 be087f48b99f
Fixed small bug that caused some definitions to be "forgotten".
src/Pure/Proof/extraction.ML
     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))