# HG changeset patch # User wenzelm # Date 878056030 -3600 # Node ID 92874142156b1692946a2580a9a099770ad75eed # Parent df6cd80b6387fcfc9093ad31c3c1676a78b4951f add_store_axioms_i; diff -r df6cd80b6387 -r 92874142156b src/Pure/axclass.ML --- 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;