# HG changeset patch
# User wenzelm
# Date 963523233 -7200
# Node ID 1a46c94d14255b18b2006e7f43697cfc21945d71
# Parent  07598d493d331236e0a1452ca3e2199fb6b29dab
defs (overloaded);

diff -r 07598d493d33 -r 1a46c94d1425 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Thu Jul 13 23:20:14 2000 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Thu Jul 13 23:20:33 2000 +0200
@@ -371,7 +371,7 @@
     val (axms_defs, axms_names) =
       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
   in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
-       "\n\n|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
+       "\n\n|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -551,7 +551,7 @@
   section "syntax" "|> Theory.add_modesyntax" syntax_decls,
   section "translations" "|> Theory.add_trrules" trans_decls,
   axm_section "rules" "|> (#1 oo (PureThy.add_axioms o map Thm.no_attributes))" axiom_decls,
-  axm_section "defs" "|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))" axiom_decls,
+  axm_section "defs" "|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,