src/HOL/Tools/record_package.ML

   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
   extfields = extfields, fieldext = fieldext }: record_data;
 
 structure RecordsArgs =
 struct
-  val name = "HOL/records";      
+  val name = "HOL/records";       
   type T = record_data;
 
   val empty =
     make_record_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}

       gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
 
 
 val parse_translation =
  [("_record_update", record_update_tr),
-  ("_update_name", update_name_tr)];
+  ("_update_name", update_name_tr)]; 
 
 val adv_parse_translation = 
  [("_record",adv_record_tr),
   ("_record_scheme",adv_record_scheme_tr),
   ("_record_type",adv_record_type_tr),
-  ("_record_type_scheme",adv_record_type_scheme_tr)];
+  ("_record_type_scheme",adv_record_type_scheme_tr)]; 
 
 (* print translations *)
 
 val print_record_type_abbr = ref true;
 val print_record_type_as_fields = ref true;

       val T = fixT (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), [])) 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;    
 
       fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T));
 
    in if !print_record_type_abbr
       then (case last_extT T of
              SOME (name,_) 
               => if name = lastExt 
                  then
-		  (let 
-                       val subst = unify schemeT T 
+		  (let
+                     val subst = unify schemeT T 
                    in 
                     if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
                     then mk_type_abbr subst abbr alphas
                     else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
 		   end handle TUNIFY => default_tr' sg tm)

 
 end;
 
 
 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
-open BasicRecordPackage;
+open BasicRecordPackage;