# HG changeset patch
# User wenzelm
# Date 878726947 -3600
# Node ID 56025371fc0297370c9e159b0e70237fb2571d3f
# Parent  a6ccec4fd0c38c7d14a8b71a0c5d2ab5f52ca3b9
tuned record_info;

diff -r a6ccec4fd0c3 -r 56025371fc02 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Wed Nov 05 11:45:51 1997 +0100
+++ b/src/HOL/thy_data.ML	Wed Nov 05 11:49:07 1997 +0100
@@ -8,7 +8,7 @@
 (*for records*)
 type record_info =
  {parent: string option,
-  selectors: (string * ctyp) list};
+  fields: (string * ctyp) list};
 
 (*for datatypes*)
 type datatype_info =
@@ -96,11 +96,11 @@
       fun pretty_parent None = []
         | pretty_parent (Some name) = [Pretty.str (name ^ " +")];
 
-      fun pretty_sel (c, T) = Pretty.block
+      fun pretty_field (c, T) = Pretty.block
         [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Display.pretty_ctyp T)];
 
-      fun pretty_record (name, {parent, selectors}) =
-        Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_sel selectors);
+      fun pretty_record (name, {parent, fields}) =
+        Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_field fields);
     in
       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
     end;