src/Pure/Proof/extraction.ML
changeset 13793 c02c81fd11b8
parent 13732 f8badfef5cf2
child 14472 cba7c0a3ffb3
--- 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'',