# HG changeset patch
# User blanchet
# Date 1409777255 -7200
# Node ID 2412a3369c3021b7210edf785f5b58012e4b95e5
# Parent  e51b4c7685a91afd1db88a10f2cf311148e6bf19
tuned BNF database handling

diff -r e51b4c7685a9 -r 2412a3369c30 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Sep 03 22:47:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Sep 03 22:47:35 2014 +0200
@@ -14,6 +14,7 @@
 
   val morph_bnf: morphism -> bnf -> bnf
   val morph_bnf_defs: morphism -> bnf -> bnf
+  val transfer_bnf: theory -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val bnf_of_global: theory -> string -> bnf option
   val bnf_interpretation: (bnf -> theory -> theory) -> theory -> theory
@@ -515,6 +516,8 @@
 
 fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
 
+val transfer_bnf = morph_bnf o Morphism.transfer_morphism;
+
 structure Data = Generic_Data
 (
   type T = bnf Symtab.table;
@@ -524,8 +527,7 @@
 );
 
 fun bnf_of_generic context =
-  Option.map (morph_bnf (Morphism.transfer_morphism (Context.theory_of context)))
-  o Symtab.lookup (Data.get context);
+  Option.map (transfer_bnf (Context.theory_of context)) o Symtab.lookup (Data.get context);
 
 val bnf_of = bnf_of_generic o Context.Proof;
 val bnf_of_global = bnf_of_generic o Context.Theory;
@@ -1516,19 +1518,18 @@
   val eq: T * T -> bool = op = o pairself T_of_bnf;
 );
 
-(* FIXME naming *)
 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"*)
+        (* arbitrarily use "Fun" as prefix for "fun" *)
         (_, [], @{type_name fun}) => [(Context.theory_name @{theory Fun}, false)]
-      | (_, qs, _) => qs)
+      | (_, qs, _) => qs);
   in
     thy
     |> Sign.root_path
     |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
-    |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
+    |> (fn thy => f (transfer_bnf thy bnf) thy)
     |> Sign.restore_naming thy
   end;
 
@@ -1537,7 +1538,8 @@
 fun register_bnf key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)))
-  #> Local_Theory.background_theory (BNF_Interpretation.data bnf);
+  #> Local_Theory.background_theory
+    (fn thy => BNF_Interpretation.data (the (bnf_of_global thy key)) thy);
 
 fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
diff -r e51b4c7685a9 -r 2412a3369c30 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 03 22:47:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 03 22:47:35 2014 +0200
@@ -168,7 +168,7 @@
   thy
   |> Sign.root_path
   |> Sign.add_path (Long_Name.qualifier s)
-  |> f fp_sugars
+  |> f (map (transfer_fp_sugar thy) fp_sugars)
   |> Sign.restore_naming thy;
 
 fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
@@ -179,7 +179,8 @@
         (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
     fp_sugars
   #> fp = Least_FP ? generate_lfp_size fp_sugars
-  #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
+  #> Local_Theory.background_theory (fn thy => FP_Sugar_Interpretation.data
+    (map (the o fp_sugar_of_global thy o fst o dest_Type o #T) fp_sugars) thy);
 
 fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
     ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss