src/Pure/theory.ML
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);