# 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))