centralized and cleaned up naming handling

--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Sep 04 14:02:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:00 2014 +0200
@@ -1521,22 +1521,9 @@
   val eq: T * T -> bool = op = o pairself T_of_bnf;
 );
 
-fun with_repaired_path f bnf thy =
-  let
-    val qualifiers =
-      (case Binding.dest (name_of_bnf bnf) of
-        (* arbitrarily use "Fun" as prefix for "fun" *)
-        (_, [], @{type_name fun}) => [(Context.theory_name @{theory Fun}, false)]
-      | (_, qs, _) => qs);
-  in
-    thy
-    |> Sign.root_path
-    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
-    |> (fn thy => f (transfer_bnf thy bnf) thy)
-    |> Sign.restore_naming thy
-  end;
+fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
 
-val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
+val bnf_interpretation = BNF_Interpretation.interpretation o with_transfer_bnf;
 val interpret_bnf = BNF_Interpretation.data;
 
 fun register_bnf_raw key bnf =

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 04 14:02:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:00 2014 +0200
@@ -223,14 +223,9 @@
   val eq: T * T -> bool = op = o pairself (map #T);
 );
 
-fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier s)
-  |> f (map (transfer_fp_sugar thy) fp_sugars)
-  |> Sign.restore_naming thy;
+fun with_transfer_fp_sugar g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
 
-val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
+val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_transfer_fp_sugar;
 val interpret_fp_sugars = FP_Sugar_Interpretation.data;
 
 fun register_fp_sugars_raw fp_sugars =

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 04 14:02:37 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:00 2014 +0200
@@ -177,14 +177,9 @@
   val eq: T * T -> bool = op = o pairself #ctrs;
 );
 
-fun with_repaired_path g (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
-  |> (fn thy => g (transfer_ctr_sugar thy ctr_sugar) thy)
-  |> Sign.restore_naming thy;
+fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar thy ctr_sugar) thy;
 
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
+val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_transfer_ctr_sugar;
 
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}

--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Thu Sep 04 14:02:37 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Fri Sep 05 00:41:00 2014 +0200
@@ -26,22 +26,24 @@
 structure Interp = Theory_Data
 (
   type T =
-    T list
-    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp) * T list) list;
+    (Name_Space.naming * T) list
+    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp)
+       * (Name_Space.naming * T) list) list;
   val empty = ([], []);
   val extend = I;
   fun merge ((data1, interps1), (data2, interps2)) : T =
-    (Library.merge eq (data1, data2),
-     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
+    (Library.merge (eq_snd eq) (data1, data2),
+     AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2));
 );
 
-val result = #1 o Interp.get;
+val result = map snd o fst o Interp.get;
 
 fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
   let
     val (data, interps) = Interp.get thy;
-    val unfinished = interps |> map (fn ((gf, _), xs) =>
-      (g_or_f gf, if eq_list eq (xs, data) then [] else subtract eq xs data));
+    val unfinished = interps |> map (fn ((gf, _), data') =>
+      (g_or_f gf,
+       if eq_list (eq_snd eq) (data', data) then [] else subtract (eq_snd eq) data' data));
     val finished = interps |> map (apsnd (K data));
   in
     if forall (null o #2) unfinished then
@@ -52,14 +54,23 @@
   end;
 
 fun consolidate lthy =
-  consolidate_common snd Local_Theory.background_theory (Proof_Context.theory_of lthy) lthy;
-fun consolidate_global thy = consolidate_common fst I thy thy;
+  consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory
+    (Proof_Context.theory_of lthy) lthy;
+
+fun consolidate_global thy =
+  consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
+    thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
 
 fun interpretation g f =
   Interp.map (apsnd (cons (((g, f), stamp ()), []))) #> perhaps consolidate_global;
 
-fun data x = Local_Theory.background_theory (Interp.map (apfst (cons x))) #> perhaps consolidate;
-fun data_global x = Interp.map (apfst (cons x)) #> perhaps consolidate_global;
+fun data x =
+  Local_Theory.background_theory (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
+  #> perhaps consolidate;
+
+fun data_global x =
+  (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
+  #> perhaps consolidate_global;
 
 val init = Theory.at_begin consolidate_global;