changeset 33039 | 5018f6a76b3f |
parent 33029 | 2fefe039edf1 |
parent 33038 | 8f9594c31de4 |
child 33049 | c38f02fdf35d |
--- a/src/HOL/Tools/record.ML Wed Oct 21 16:41:22 2009 +1100 +++ b/src/HOL/Tools/record.ML Wed Oct 21 08:16:25 2009 +0200 @@ -1834,7 +1834,7 @@ val extN = full bname; val types = map snd fields; val alphas_fields = fold Term.add_tfree_namesT types []; - val alphas_ext = alphas inter alphas_fields; + val alphas_ext = inter (op =) (alphas, alphas_fields); val len = length fields; val variants = Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)