# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID f5ee068b96a67aa8693a1c7778fbc4c73dfbafad
# Parent  f3248e77c96023365327b07c05cbc11d2d51652b
generalized ML function

diff -r f3248e77c960 -r f5ee068b96a6 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -2174,7 +2174,7 @@
              xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
              xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
-      fixpoint_bnf (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
+      fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
         (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
diff -r f3248e77c960 -r f5ee068b96a6 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -246,7 +246,7 @@
 
         val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fixpoint_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress)
+          fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress)
             fp_bs unsorted_As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
 
         val time = time lthy;
diff -r f3248e77c960 -r f5ee068b96a6 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -197,8 +197,9 @@
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
-  val fixpoint_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
-      BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
+  val fixpoint_bnf: (binding -> binding) ->
+      (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+      BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
     BNF_Comp.comp_cache -> local_theory ->
     ((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a
@@ -610,7 +611,7 @@
     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   end;
 
-fun fixpoint_bnf construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
+fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -628,7 +629,7 @@
       in
         Binding.prefix_name rawN
         #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
-        #> Binding.concealed
+        #> extra_qualify #> Binding.concealed
       end;
 
     val ((bnfs, (deadss, livess)), (comp_cache, unfold_set)) =
@@ -637,8 +638,9 @@
           (fn b => bnf_of_typ true Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
           ((comp_cache0, empty_unfolds), lthy));
 
-    fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
-      #> Binding.concealed;
+    fun norm_qualify i =
+      Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
+      #> extra_qualify #> Binding.concealed;
 
     val Ass = map (map dest_TFree) livess;
     val Ds' = fold (fold Term.add_tfreesT) deadss [];
@@ -654,7 +656,9 @@
 
     val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
-    fun pre_qualify b = Binding.qualify false (Binding.name_of b)
+    fun pre_qualify b =
+      Binding.qualify false (Binding.name_of b)
+      #> extra_qualify
       #> not (Config.get lthy' bnf_internals) ? Binding.concealed;
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy'') =