src/Pure/theory.ML

--- a/src/Pure/theory.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/theory.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -177,7 +177,7 @@
 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
-    val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
+    val (_, axioms') = Name_Space.define (Sign.inherit_naming thy ctxt) true axm axioms;
   in axioms' end);