# HG changeset patch
# User wenzelm
# Date 893841274 -7200
# Node ID fdc7d8949d82600a5b1d8cee718713e474b1c532
# Parent  4fb63c77f2df922c9a6d03f95aa60e0b6b7edb08
adapted to new PureThy.add_axioms_i;

diff -r 4fb63c77f2df -r fdc7d8949d82 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 29 11:13:22 1998 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 29 11:14:34 1998 +0200
@@ -217,7 +217,8 @@
     val intro_axm = Logic.list_implies
       (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   in
-    PureThy.add_store_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy
+    thy
+    |> PureThy.add_axioms_i (map Attribute.none ((raw_class ^ "I", intro_axm) :: abs_axioms))
   end;