src/Pure/axclass.ML

     fun inclass c = Logic.mk_inclass (aT axS, c);
 
     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;
 
 
 (* external interfaces *)