suppress irrelevant position reports;

--- 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);
 
 

--- a/src/Pure/variable.ML	Mon Dec 28 16:13:15 2015 +0100
+++ b/src/Pure/variable.ML	Mon Dec 28 16:29:39 2015 +0100
@@ -409,7 +409,9 @@
   else
     let
       val proper = Config.get ctxt proper_fixes;
-      val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
+      val context = Context.Proof ctxt
+        |> Name_Space.map_naming (K Name_Space.global_naming)
+        |> Context_Position.set_visible_generic false;
     in
       ctxt
       |> map_fixes