# HG changeset patch # User wenzelm # Date 1008973107 -3600 # Node ID 3573830e9b918150afb8424aa02d8e50977b7543 # Parent afc6ffffeb11ebb32777e4f49fc9ed51d1dcec8b hide base name of "make", "fields", "extend", "truncate", "more", "more_update"; diff -r afc6ffffeb11 -r 3573830e9b91 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Fri Dec 21 23:17:35 2001 +0100 +++ b/src/HOL/Tools/record_package.ML Fri Dec 21 23:18:27 2001 +0100 @@ -848,7 +848,9 @@ |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs |>>> (PureThy.add_defs_i false o map Thm.no_attributes) - [make_spec, fields_spec, extend_spec, truncate_spec]; + [make_spec, fields_spec, extend_spec, truncate_spec] + |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN, + full moreN, full (suffix updateN moreN)]; (* 3rd stage: thms_thy *)