# HG changeset patch
# User wenzelm
# Date 1427816092 -7200
# Node ID 30687c3f2b10d19268c16d4414c54990ce16056f
# Parent  6292f1f5ffae487c35805f74fa7cbd2fe582a0da
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;

diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Library/Code_Test.thy	Tue Mar 31 17:34:52 2015 +0200
@@ -64,7 +64,7 @@
 by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
 
 context begin
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "xml") *}
 
 type_synonym attributes = "(String.literal \<times> String.literal) list"
 type_synonym body = "xml_tree list"
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -529,7 +529,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       thy3
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}
@@ -1505,7 +1505,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = false, no_ind = false, skip_mono = true}
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Product_Type.thy	Tue Mar 31 17:34:52 2015 +0200
@@ -988,7 +988,7 @@
 context
 begin
 
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "prod") *}
 
 definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
 where
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -145,9 +145,9 @@
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.concealed
+      |> Proof_Context.concealed
       |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
-      ||> Local_Theory.restore_naming lthy
+      ||> Proof_Context.restore_naming lthy
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -445,7 +445,7 @@
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
       lthy
-      |> Local_Theory.concealed
+      |> Proof_Context.concealed
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,
@@ -458,7 +458,7 @@
           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
-      ||> Local_Theory.restore_naming lthy
+      ||> Proof_Context.restore_naming lthy
 
     fun requantify orig_intro thm =
       let
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -172,7 +172,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       thy1
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -146,7 +146,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       thy0
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
             coind = false, no_elim = false, no_ind = true, skip_mono = true}
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -843,13 +843,13 @@
 
     val is_auxiliary = length cs >= 2; 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> is_auxiliary ? Local_Theory.concealed
+      |> is_auxiliary ? Proof_Context.concealed
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> is_auxiliary ? Local_Theory.restore_naming lthy;
+      ||> Proof_Context.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
         (Thm.cterm_of lthy' (list_comb (rec_const, params)));
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -488,13 +488,13 @@
 
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
-      |> Local_Theory.concealed  (* FIXME ?? *)
+      |> Proof_Context.concealed  (* FIXME ?? *)
       |> fold_map Local_Theory.define
         (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
            (cnames_syn ~~ cs_info ~~ preds))
-      ||> Local_Theory.restore_naming lthy1;
+      ||> Proof_Context.restore_naming lthy1;
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold
diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -81,10 +81,10 @@
   Typedef_Plugin.interpretation typedef_plugin
     (fn name => fn lthy =>
       lthy
-      |> Local_Theory.map_naming
+      |> Local_Theory.map_background_naming
           (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
       |> f name
-      |> Local_Theory.restore_naming lthy);
+      |> Local_Theory.restore_background_naming lthy);
 
 
 (* primitive typedef axiomatization -- for fresh typedecl *)
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -98,7 +98,7 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.open_target
-      (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
+      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   end;
 
 in
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -25,13 +25,13 @@
     local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
-  val naming_of: local_theory -> Name_Space.naming
+  val background_naming_of: local_theory -> Name_Space.naming
+  val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
+    local_theory -> local_theory
+  val restore_background_naming: local_theory -> local_theory -> local_theory
   val full_name: local_theory -> binding -> string
-  val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
-  val concealed: local_theory -> local_theory
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
-  val restore_naming: local_theory -> local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -97,15 +97,15 @@
   exit: local_theory -> Proof.context};
 
 type lthy =
- {naming: Name_Space.naming,
+ {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
-  {naming = naming, operations = operations, after_close = after_close,
-    brittle = brittle, target = target};
+fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+  {background_naming = background_naming, operations = operations,
+    after_close = after_close, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -124,8 +124,8 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
-    make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
 
 fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
@@ -144,9 +144,9 @@
     else lthy
   end;
 
-fun open_target naming operations after_close target =
+fun open_target background_naming operations after_close target =
   assert target
-  |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
+  |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
 
 fun close_target lthy =
   let
@@ -156,13 +156,14 @@
 
 fun map_contexts f lthy =
   let val n = level lthy in
-    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
-      make_lthy (naming, operations, after_close, brittle,
-        target
-        |> Context_Position.set_visible false
-        |> f (n - i - 1)
-        |> Context_Position.restore_visible target))
-    |> f n
+    lthy |> (Data.map o map_index)
+      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
+        make_lthy (background_naming, operations, after_close, brittle,
+          target
+          |> Context_Position.set_visible false
+          |> f (n - i - 1)
+          |> Context_Position.restore_visible target))
+      |> f n
   end;
 
 
@@ -170,8 +171,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (naming, operations, after_close, _, target) =>
-      (naming, operations, after_close, true, target)) lthy
+    map_top (fn (background_naming, operations, after_close, _, target) =>
+      (background_naming, operations, after_close, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -179,20 +180,20 @@
   else lthy;
 
 
-(* naming *)
+(* naming for background theory *)
 
-val naming_of = #naming o top_of;
-val full_name = Name_Space.full_name o naming_of;
+val background_naming_of = #background_naming o top_of;
 
-fun map_naming f =
-  map_top (fn (naming, operations, after_close, brittle, target) =>
-    (f naming, operations, after_close, brittle, target));
+fun map_background_naming f =
+  map_top (fn (background_naming, operations, after_close, brittle, target) =>
+    (f background_naming, operations, after_close, brittle, target));
 
-val concealed = map_naming Name_Space.concealed;
-val new_group = map_naming Name_Space.new_group;
-val reset_group = map_naming Name_Space.reset_group;
+val restore_background_naming = map_background_naming o K o background_naming_of;
 
-val restore_naming = map_naming o K o naming_of;
+val full_name = Name_Space.full_name o background_naming_of;
+
+val new_group = map_background_naming Name_Space.new_group;
+val reset_group = map_background_naming Name_Space.reset_group;
 
 
 (* standard morphisms *)
@@ -200,7 +201,7 @@
 fun standard_morphism lthy ctxt =
   Proof_Context.norm_export_morphism lthy ctxt $>
   Morphism.binding_morphism "Local_Theory.standard_binding"
-    (Name_Space.transform_binding (naming_of lthy));
+    (Name_Space.transform_binding (Proof_Context.naming_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
@@ -219,7 +220,7 @@
 fun background_theory_result f lthy =
   lthy |> raw_theory_result (fn thy =>
     thy
-    |> Sign.map_naming (K (naming_of lthy))
+    |> Sign.map_naming (K (background_naming_of lthy))
     |> f
     ||> Sign.restore_naming thy);
 
@@ -343,9 +344,9 @@
 
 (* init *)
 
-fun init naming operations target =
+fun init background_naming operations target =
   target |> Data.map
-    (fn [] => [make_lthy (naming, operations, I, false, target)]
+    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
       | _ => error "Local theory already initialized");
 
 
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -155,14 +155,14 @@
 fun gen_init before_exit target thy =
   let
     val name_data = make_name_data thy target;
-    val naming =
+    val background_naming =
       Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
     thy
     |> Sign.change_begin
     |> init_context name_data
     |> is_none before_exit ? Data.put (SOME name_data)
-    |> Local_Theory.init naming
+    |> Local_Theory.init background_naming
        {define = Generic_Target.define (foundation name_data),
         notes = Generic_Target.notes (notes name_data),
         abbrev = Generic_Target.abbrev (abbrev name_data),
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -34,6 +34,7 @@
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
+  val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
@@ -304,6 +305,8 @@
 
 val full_name = Name_Space.full_name o naming_of;
 
+val concealed = map_naming Name_Space.concealed;
+
 
 (* name spaces *)
 
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/Tools/plugin.ML
--- a/src/Pure/Tools/plugin.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/Tools/plugin.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -138,9 +138,9 @@
 
 fun apply change_naming (interp: interp) (data: data) lthy =
   lthy
-  |> change_naming ? Local_Theory.map_naming (K (#naming data))
+  |> change_naming ? Local_Theory.map_background_naming (K (#naming data))
   |> #apply interp (#value data)
-  |> Local_Theory.restore_naming lthy;
+  |> Local_Theory.restore_background_naming lthy;
 
 fun unfinished data (interp: interp, data') =
   (interp,
diff -r 6292f1f5ffae -r 30687c3f2b10 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/Pure/sign.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -109,6 +109,7 @@
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
+  val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
   val hide_const: bool -> string -> theory -> theory
@@ -510,6 +511,8 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val concealed = map_naming Name_Space.concealed;
+
 
 (* hide names *)