Fixed bug in function corr.
authorberghofe
Wed, 29 Jan 2003 17:32:01 +0100
changeset 13793 c02c81fd11b8
parent 13792 d1811693899c
child 13794 332eb2e69a65
Fixed bug in function corr.
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'',