# HG changeset patch
# User wenzelm
# Date 1451316579 -3600
# Node ID d9acd750c1f636ed7aa6ef1a2e4ddd77e56eaee7
# Parent  52972bed8e2e92d88c9f128c997cdb5b8e5f01a0
suppress irrelevant position reports;

diff -r 52972bed8e2e -r d9acd750c1f6 src/Pure/theory.ML
--- 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);
 
 
diff -r 52972bed8e2e -r d9acd750c1f6 src/Pure/variable.ML
--- 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