# HG changeset patch
# User schirmer
# Date 1125430330 -7200
# Node ID 5fc6a0666094aabc35c8890f84d401352e7cae75
# Parent  b15f8e0948748a7a8b0b8981e726ab74aea5bec2
fixed bug in record_type_abbr_tr'

diff -r b15f8e094874 -r 5fc6a0666094 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Aug 30 12:47:53 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Aug 30 21:32:10 2005 +0200
@@ -727,7 +727,8 @@
 
       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));
 
@@ -1694,7 +1695,7 @@
     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 =