# HG changeset patch
# User schirmer
# Date 1117981430 -7200
# Node ID de9815628d33a15af9a90d0a86ae3f74839aa77e
# Parent  d7f8c48d5acb719912f885debc5d82ce5af4a88a
bugfix in record_type_abbr_tr'

diff -r d7f8c48d5acb -r de9815628d33 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun Jun 05 16:09:48 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Sun Jun 05 16:23:50 2005 +0200
@@ -236,7 +236,7 @@
 
 structure RecordsArgs =
 struct
-  val name = "HOL/records";      
+  val name = "HOL/records";       
   type T = record_data;
 
   val empty =
@@ -629,13 +629,13 @@
 
 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 *)
 
@@ -729,7 +729,7 @@
       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));
@@ -739,8 +739,8 @@
              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
@@ -2143,4 +2143,4 @@
 
 
 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
-open BasicRecordPackage;
+open BasicRecordPackage;