author | wenzelm |
Tue, 28 Oct 1997 17:27:10 +0100 | |
changeset 4015 | 92874142156b |
parent 4014 | df6cd80b6387 |
child 4016 | 90aebb69c04e |
--- 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;