src/Pure/axclass.ML
changeset 4845 fdc7d8949d82
parent 4015 92874142156b
child 4917 7c22890a7a9b
     1.1 --- a/src/Pure/axclass.ML	Wed Apr 29 11:13:22 1998 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Apr 29 11:14:34 1998 +0200
     1.3 @@ -217,7 +217,8 @@
     1.4      val intro_axm = Logic.list_implies
     1.5        (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
     1.6    in
     1.7 -    PureThy.add_store_axioms_i ((raw_class ^ "I", intro_axm) :: abs_axioms) thy
     1.8 +    thy
     1.9 +    |> PureThy.add_axioms_i (map Attribute.none ((raw_class ^ "I", intro_axm) :: abs_axioms))
    1.10    end;
    1.11  
    1.12