# HG changeset patch
# User blanchet
# Date 1428613808 -7200
# Node ID 19e5f5ac7b59fac77fa6a64b55c27640c932b348
# Parent  8f6cacc87f426018774c92dbcded935536e1a325
renamed misleading option

diff -r 8f6cacc87f42 -r 19e5f5ac7b59 src/HOL/Tools/BNF/bnf_comp.ML
--- 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