--- a/src/Pure/theory.ML Mon Dec 28 16:13:15 2015 +0100
+++ b/src/Pure/theory.ML Mon Dec 28 16:29:39 2015 +0100
@@ -206,7 +206,10 @@
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 (Sign.inherit_naming thy ctxt) true axm axioms;
+ val context = ctxt
+ |> Sign.inherit_naming thy
+ |> Context_Position.set_visible_generic false;
+ val (_, axioms') = Name_Space.define context true axm axioms;
in axioms' end);