# HG changeset patch
# User wenzelm
# Date 878056358 -3600
# Node ID f88775cc8d178e6b553032cee2efcbd3c38d9b32
# Parent  f9bfb914805ade40e28d56741d33d9f4fcfd4f95
PureThy.add_store_defs, PureThy.add_store_axioms;

diff -r f9bfb914805a -r f88775cc8d17 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Oct 28 17:31:55 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 28 17:32:38 1997 +0100
@@ -375,7 +375,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|> Theory.add_defs\n" ^ axms_defs, axms_names)
+       "\n\n|> PureThy.add_store_defs\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -554,8 +554,8 @@
   section "consts" "|> Theory.add_consts" const_decls,
   section "syntax" "|> Theory.add_modesyntax" syntax_decls,
   section "translations" "|> Theory.add_trrules" trans_decls,
-  axm_section "rules" "|> Theory.add_axioms" axiom_decls,
-  axm_section "defs" "|> Theory.add_defs" axiom_decls,
+  axm_section "rules" "|> PureThy.add_store_axioms" axiom_decls,
+  axm_section "defs" "|> PureThy.add_store_defs" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,