# HG changeset patch
# User schirmer
# Date 1115060841 -7200
# Node ID 530099d1a73ce99d78195bbf63c4fa22421135ec
# Parent  47aa1a8fcdc9d76fab82fcfad68bcf8de11aa705
Removed nodup_vars avoiding hack

diff -r 47aa1a8fcdc9 -r 530099d1a73c src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon May 02 19:00:05 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon May 02 21:07:21 2005 +0200
@@ -1480,9 +1480,8 @@
                             (cterm_of sg (Free (variant variants (base c ^ "'"),T))); 
         val refls = map mkrefl fields_more;
         val constr_refl = Thm.reflexive (cterm_of sg (head_of ext));
-        val dest_convs' = map (Thm.freezeT o mk_meta_eq) dest_convs;
-         (* freezeT just for performance, to adjust the maxidx, so that nodup_vars will not 
-                be called during combination *)
+        val dest_convs' = map mk_meta_eq dest_convs;
+         
         fun mkthm (udef,(fld_refl,thms)) =
           let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
                (* (|N=N (|N=N,M=M,K=K,more=more|)