# HG changeset patch
# User wenzelm
# Date 1005342684 -3600
# Node ID 964f5ffe13d001faacb4368769fccef4d8d1fb69
# Parent  25565bbbd246b06bc311c1b1a5706abbf2548781
fixed print_records;

diff -r 25565bbbd246 -r 964f5ffe13d0 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Nov 09 22:50:58 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Nov 09 22:51:24 2001 +0100
@@ -384,23 +384,20 @@
   fun print sg ({records = recs, ...}: record_data) =
     let
       val prt_typ = Sign.pretty_typ sg;
-      val ext_const = Sign.cond_extern sg Sign.constK;
 
       fun pretty_parent None = []
         | pretty_parent (Some (Ts, name)) =
             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
 
       fun pretty_field (c, T) = Pretty.block
-        [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)];
+        [Pretty.str (Sign.cond_extern sg Sign.constK c), Pretty.str " ::",
+          Pretty.brk 1, Pretty.quote (prt_typ T)];
 
       fun pretty_record (name, {args, parent, fields, simps = _, induct = _, cases = _}) =
         Pretty.block (Pretty.fbreaks (Pretty.block
           [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
           pretty_parent parent @ map pretty_field fields));
-    in
-      map pretty_record (Sign.cond_extern_table sg Sign.typeK recs)
-      |> Pretty.chunks |> Pretty.writeln
-    end;
+    in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
 end;
 
 structure RecordsData = TheoryDataFun(RecordsArgs);