tuned record_info;
authorwenzelm
Wed Nov 05 11:49:07 1997 +0100 (1997-11-05)
changeset 415056025371fc02
parent 4149 a6ccec4fd0c3
child 4151 5c19cd418c33
tuned record_info;
src/HOL/thy_data.ML
     1.1 --- a/src/HOL/thy_data.ML	Wed Nov 05 11:45:51 1997 +0100
     1.2 +++ b/src/HOL/thy_data.ML	Wed Nov 05 11:49:07 1997 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  (*for records*)
     1.5  type record_info =
     1.6   {parent: string option,
     1.7 -  selectors: (string * ctyp) list};
     1.8 +  fields: (string * ctyp) list};
     1.9  
    1.10  (*for datatypes*)
    1.11  type datatype_info =
    1.12 @@ -96,11 +96,11 @@
    1.13        fun pretty_parent None = []
    1.14          | pretty_parent (Some name) = [Pretty.str (name ^ " +")];
    1.15  
    1.16 -      fun pretty_sel (c, T) = Pretty.block
    1.17 +      fun pretty_field (c, T) = Pretty.block
    1.18          [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Display.pretty_ctyp T)];
    1.19  
    1.20 -      fun pretty_record (name, {parent, selectors}) =
    1.21 -        Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_sel selectors);
    1.22 +      fun pretty_record (name, {parent, fields}) =
    1.23 +        Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_field fields);
    1.24      in
    1.25        seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
    1.26      end;