Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/ax_ops/thy_ops.ML
changeset 4029 22f2d1b17f97
parent 4008 2444085532c6 
--- 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;
isabelle