changeset 30466 | 5f31e24937c5 |
parent 30337 | eb189f7e43a1 |
child 32789 | d89327de0b3c |
--- a/src/Pure/theory.ML Thu Mar 12 11:09:26 2009 +0100 +++ b/src/Pure/theory.ML Thu Mar 12 11:10:02 2009 +0100 @@ -175,7 +175,7 @@ fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms => let val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms; - val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms + val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms handle Symtab.DUP dup => err_dup_axm dup; in axioms' end);