--- 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