author | wenzelm |
Wed, 29 Apr 1998 11:14:34 +0200 | |
changeset 4845 | fdc7d8949d82 |
parent 4844 | 4fb63c77f2df |
child 4846 | 9c072489a9e7 |
--- 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;