src/HOLCF/ax_ops/thy_ops.ML

       val syndecls = syn_decls curried sign decls;
       val xrules = xrules_of curried decls;
       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;
 
 fun add_ops_i {curried,strict,total} decls thy =
   let val {sign,...} = rep_theory thy;

       val syndecls = syn_decls curried sign decls;
       val xrules = xrules_of curried decls;
       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;
 
 
 (* parser: ops_decls ********************************)