src/HOL/Tools/record.ML
changeset 56254 a2dd9200854d
parent 56249 0fda98dd2c93
child 56513 34ea4d7f236c
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -1819,7 +1819,7 @@
     1.4      val all_vars = parent_vars @ vars;
     1.5      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
     1.6  
     1.7 -    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
     1.8 +    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
     1.9      val moreT = TFree zeta;
    1.10      val more = Free (moreN, moreT);
    1.11      val full_moreN = full (Binding.name moreN);