# 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 *)