src/HOL/BNF/Tools/bnf_comp.ML

     (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
     (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
     (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
-  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
-    (BNF_Def.bnf * typ list) * local_theory
+  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf ->
+    Proof.context -> (BNF_Def.bnf * typ list) * local_theory
 end;
 
 structure BNF_Comp : BNF_COMP =
 struct
 

     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
         [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
-
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
 
 (* Changing the order of live variables *)

       (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))
   end;
 
 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
 
-fun seal_bnf (unfold_set : unfold_set) b Ds bnf lthy =
+fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     val (As, lthy1) = apfst (map TFree)

     val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
     val T = mk_T_of_bnf Ds As bnf;
 
     (*bd should only depend on dead type variables!*)
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
-    val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
+    val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
     val params = fold Term.add_tfreesT Ds [];
     val deads = map TFree params;
 
     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
       typedef (bdT_bind, params, NoSyn)

 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
-      Binding.empty Binding.empty []
-      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+    val (bnf', lthy') =
+      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
+        Binding.empty Binding.empty []
+        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
   end;
 
 exception BAD_DEAD of typ * typ;