# HG changeset patch
# User berghofe
# Date 1037573033 -3600
# Node ID 44fed7d0c305298adc695575c7c4d907ca801cc0
# Parent  9f94248d2f5a06334c19fdd7ce66dd049abd2d9e
Fixed small bug that caused some definitions to be "forgotten".

diff -r 9f94248d2f5a -r 44fed7d0c305 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Nov 16 23:01:59 2002 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 17 23:43:53 2002 +0100
@@ -478,7 +478,7 @@
                     val args = vfs_of prop;
                     val corr_prf' = foldr forall_intr_prf (args, corr_prf);
                   in
-                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs',
+                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs'',
                      prf_subst_TVars tye' corr_prf')
                   end
               | Some (_, prf') => (defs', prf_subst_TVars tye' prf'))
@@ -580,7 +580,7 @@
                                   Some (map TVar (term_tvars eqn))))) %%
                             corr_prf)))
                   in
-                    ((s, (vs', ((t', u), corr_prf'))) :: defs',
+                    ((s, (vs', ((t', u), corr_prf'))) :: defs'',
                      subst_TVars tye' u)
                   end
               | Some ((_, u), _) => (defs, subst_TVars tye' u))