--- 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,