# HG changeset patch
# User wenzelm
# Date 1117533195 -7200
# Node ID 8340f7ca96d02bdd27808234642fa11b5cf700d9
# Parent  1381e90c2694764f2ecf8c4115790f27b1cc3fe7
renamed cond_extern to extern;
NameSpace.qualified;

diff -r 1381e90c2694 -r 8340f7ca96d0 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue May 31 11:53:14 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue May 31 11:53:15 2005 +0200
@@ -287,7 +287,7 @@
             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
 
       fun pretty_field (c, T) = Pretty.block
-        [Pretty.str (Sign.cond_extern sg Sign.constK c), Pretty.str " ::",
+        [Pretty.str (Sign.extern sg Sign.constK c), Pretty.str " ::",
           Pretty.brk 1, Pretty.quote (prt_typ T)];
 
       fun pretty_record (name, {args, parent, fields, ...}: record_info) =
@@ -1715,11 +1715,11 @@
     
     fun parent_more s = 
          if null parents then s 
-         else mk_sel s (NameSpace.append (#name (hd (rev parents))) moreN, extT);
+         else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
 
     fun parent_more_upd v s =
       if null parents then v 
-      else let val mp = (NameSpace.append (#name (hd (rev parents))) moreN);
+      else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
            in mk_upd updateN mp v s end;
    
     (*record (scheme) type abbreviation*)