# HG changeset patch
# User berghofe
# Date 1043857921 -3600
# Node ID c02c81fd11b8847fa8e920d646a16bf1b6cbb8d9
# Parent  d1811693899c67a60a377b51ade1b16d84dd3811
Fixed bug in function corr.

diff -r d1811693899c -r c02c81fd11b8 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Jan 29 16:34:51 2003 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Jan 29 17:32:01 2003 +0100
@@ -537,7 +537,7 @@
                     val corr_prop = Reconstruct.prop_of corr_prf;
                     val corr_prf' = foldr forall_intr_prf
                       (map (get_var_type corr_prop) (vfs_of prop), proof_combt
-                         (PThm ((corr_name name vs, []), corr_prf, corr_prop,
+                         (PThm ((corr_name name vs', []), corr_prf, corr_prop,
                              Some (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
                   in
                     ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',