--- 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|)