add_store_axioms_i;
authorwenzelm
Tue, 28 Oct 1997 17:27:10 +0100
changeset 4015 92874142156b
parent 4014 df6cd80b6387
child 4016 90aebb69c04e
add_store_axioms_i;
src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Oct 28 14:03:25 1997 +0100
+++ b/src/Pure/axclass.ML	Tue Oct 28 17:27:10 1997 +0100
@@ -33,6 +33,7 @@
 structure AxClass : AX_CLASS =
 struct
 
+
 (** utilities **)
 
 (* type vars *)
@@ -216,7 +217,7 @@
     val intro_axm = Logic.list_implies
       (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   in
-    Theory.add_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy
+    PureThy.add_store_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy
   end;