PureThy.add_store_axioms_i;

--- a/src/HOLCF/ax_ops/thy_axioms.ML	Tue Oct 28 17:58:08 1997 +0100
+++ b/src/HOLCF/ax_ops/thy_axioms.ML	Tue Oct 28 17:58:35 1997 +0100
@@ -148,7 +148,7 @@
   let val {sign, ...} = rep_theory theory;
       val constraints = get_constraints_of_str sign (defvarlist@varlist)
   in
-    Theory.add_axioms_i (map (apsnd 
+    PureThy.add_store_axioms_i (map (apsnd 
      (check_and_extend sign (map fst defvarlist) (map fst varlist)) o
                (read_ext_axm sign constraints)) axioms) theory
   end 
@@ -157,7 +157,7 @@
   let val {sign, ...} = rep_theory theory;
       val constraints = get_constraints_of_typ sign (defvarlist@varlist)
   in
-    Theory.add_axioms_i (map (apsnd (check_and_extend sign 
+    PureThy.add_store_axioms_i (map (apsnd (check_and_extend sign 
                                (map fst defvarlist) (map fst varlist)) o
                    (read_ext_axm_terms sign constraints)) axiom_terms) theory
   end

--- a/src/HOLCF/ax_ops/thy_ops.ML	Tue Oct 28 17:58:08 1997 +0100
+++ b/src/HOLCF/ax_ops/thy_ops.ML	Tue Oct 28 17:58:35 1997 +0100
@@ -340,7 +340,7 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
+  Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms) 
                      (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   end;
 
@@ -352,7 +352,7 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
+  Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms) 
                      (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   end;