changeset 33049 | c38f02fdf35d |
parent 33039 | 5018f6a76b3f |
child 33055 | 5a733f325939 |
--- a/src/HOL/Tools/record.ML Wed Oct 21 10:15:31 2009 +0200 +++ b/src/HOL/Tools/record.ML Wed Oct 21 12:09:37 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 = inter (op =) (alphas, alphas_fields); + val alphas_ext = inter (op =) alphas_fields alphas; val len = length fields; val variants = Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)