expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;

--- a/src/Pure/Isar/expression.ML	Wed Sep 02 15:49:12 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Sep 02 16:01:57 2015 +0200
@@ -683,9 +683,8 @@
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
-      |> Sign.declare_const_global ((Binding.concealed binding, predT), NoSyn) |> snd
-      |> Global_Theory.add_defs false
-        [((Binding.concealed (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
+      |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd
+      |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])];
     val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement
@@ -730,7 +729,7 @@
             thy'
             |> Sign.qualified_path true abinding
             |> Global_Theory.note_thmss ""
-              [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
+              [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro, axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
@@ -745,8 +744,8 @@
             thy'''
             |> Sign.qualified_path true binding
             |> Global_Theory.note_thmss ""
-                 [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.intro_add])]),
-                  ((Binding.concealed (Binding.name axiomsN), []),
+                 [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
+                  ((Binding.name axiomsN, []),
                     [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
                       [])])]
             ||> Sign.restore_naming thy''';
@@ -815,7 +814,7 @@
 
     val notes =
       if is_some asm then
-        [("", [((Binding.concealed (Binding.suffix_name ("_" ^ axiomsN) binding), []),
+        [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
           [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
             [(Attrib.internal o K) Locale.witness_add])])])]
       else [];