src/HOL/Tools/BNF/bnf_comp.ML

 Composition of bounded natural functors.
 *)
 
 signature BNF_COMP =
 sig
-  val bnf_inline_threshold: int Config.T
+  val inline_threshold: int Config.T
 
   val ID_bnf: BNF_Def.bnf
   val DEADID_bnf: BNF_Def.bnf
 
   type comp_cache

 open BNF_Def
 open BNF_Util
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-val bnf_inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
+val inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
 
 val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
 val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
 
 type comp_cache = (bnf * (typ list * typ list)) Typtab.table;

 val mk_abs = mk_abs_or_rep range_type;
 val mk_rep = mk_abs_or_rep domain_type;
 
 fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
   let
-    val threshold = Config.get ctxt bnf_inline_threshold;
+    val threshold = Config.get ctxt inline_threshold;
     val repT = HOLogic.dest_setT (fastype_of set);
     val out_of_line = force_out_of_line orelse
       (threshold >= 0 andalso Term.size_of_typ repT > threshold);
   in
     if out_of_line then