--- a/src/HOL/Tools/record.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 22 18:19:57 2014 +0100
@@ -1819,7 +1819,7 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
+ val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);