# HG changeset patch
# User wenzelm
# Date 901805099 -7200
# Node ID 2bc5b5cf051603bd32ebd7bd85af8b69e783abbf
# Parent  c02b0c72778055f910e0bddffea2fad2b60f4b7c
make_defs not marked as internal;

diff -r c02b0c727780 -r 2bc5b5cf0516 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 29 15:38:08 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jul 30 15:24:59 1998 +0200
@@ -593,7 +593,8 @@
       |> (Theory.add_consts_i o map Syntax.no_syn)
         (sel_decls @ update_decls @ make_decls)
       |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
-        (sel_specs @ update_specs @ make_specs);
+        (sel_specs @ update_specs)
+      |> (PureThy.add_defs_i o map Attribute.none) make_specs;
 
     val sel_defs = get_defs defs_thy sel_specs;
     val update_defs = get_defs defs_thy update_specs;