changeset 33038 | 8f9594c31de4 |
parent 33037 | b22e44496dc2 |
child 33039 | 5018f6a76b3f |
--- a/src/HOL/Tools/record.ML Tue Oct 20 16:13:01 2009 +0200 +++ b/src/HOL/Tools/record.ML Wed Oct 21 08:14:38 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 = gen_inter (op =) (alphas, 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)