src/HOL/Tools/record_package.ML

 
       val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
       val tsig = Sign.tsig_of sg
 
       fun mk_type_abbr subst name alphas = 
-          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
+          let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas);
           in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
 
       fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
 
    in if !print_record_type_abbr