# HG changeset patch
# User wenzelm
# Date 878056030 -3600
# Node ID 92874142156b1692946a2580a9a099770ad75eed
# Parent  df6cd80b6387fcfc9093ad31c3c1676a78b4951f
add_store_axioms_i;

diff -r df6cd80b6387 -r 92874142156b 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;