# 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;