src/HOLCF/ax_ops/thy_ops.ML
changeset 3771 ede66fb99880
parent 3621 d3e248853428
child 4008 2444085532c6
--- a/src/HOLCF/ax_ops/thy_ops.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -342,8 +342,8 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
-                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
+  Theory.add_trrules_i xrules (Theory.add_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 =
@@ -354,8 +354,8 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
-                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
+  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
+                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   end;