--- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Apr 09 22:56:31 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Apr 09 23:10:08 2015 +0200
@@ -8,7 +8,7 @@
signature BNF_COMP =
sig
- val inline_threshold: int Config.T
+ val typedef_threshold: int Config.T
val ID_bnf: BNF_Def.bnf
val DEADID_bnf: BNF_Def.bnf
@@ -76,7 +76,7 @@
open BNF_Tactics
open BNF_Comp_Tactics
-val inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
+val typedef_threshold = Attrib.setup_config_int @{binding bnf_typedef_threshold} (K 6);
val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
@@ -755,10 +755,10 @@
fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
let
- val threshold = Config.get ctxt inline_threshold;
+ val threshold = Config.get ctxt typedef_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);
+ (threshold >= 0 andalso Term.size_of_typ repT >= threshold);
in
if out_of_line then
typedef (b, As, mx) set opt_morphs tac