src/HOL/Tools/record_package.ML

       val T = fixT (Sign.intern_typ sg 
                       (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); 
 
       fun mk_type_abbr subst name alphas = 
           let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas);
-          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
+          in Syntax.term_of_typ (! Syntax.show_sorts) 
+               (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end;    
 
       fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0));
 
    in if !print_record_type_abbr
       then (case last_extT T of

     in map (gen_record_tr') trnames end;
 
     val adv_record_type_abbr_tr's =
       let val trnames = NameSpace.accesses' (hd extension_names);
           val lastExt = (unsuffix ext_typeN (fst extension));
-      in map (gen_record_type_abbr_tr' bname alphas zeta lastExt rec_schemeT0) trnames
+      in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames
       end;
 
     val adv_record_type_tr's =
       let val trnames = if parent_len > 0 then NameSpace.accesses' extN else [];
                         (* avoid conflict with adv_record_type_abbr_tr's *)