# HG changeset patch
# User blanchet
# Date 1473153681 -7200
# Node ID 6489d85ecc984212191628404f990992d3ed2968
# Parent  737d424cbac9a3eba85df187103acf7514e21025
extended ML signature

diff -r 737d424cbac9 -r 6489d85ecc98 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Sep 06 10:28:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Sep 06 11:21:21 2016 +0200
@@ -9,6 +9,10 @@
 signature BNF_COMP =
 sig
   val typedef_threshold: int Config.T
+  val with_typedef_threshold: int -> (Proof.context -> Proof.context) -> Proof.context ->
+    Proof.context
+  val with_typedef_threshold_yield: int -> (Proof.context -> 'a * Proof.context) -> Proof.context ->
+    'a * Proof.context
 
   val ID_bnf: BNF_Def.bnf
   val DEADID_bnf: BNF_Def.bnf
@@ -78,6 +82,18 @@
 
 val typedef_threshold = Attrib.setup_config_int @{binding bnf_typedef_threshold} (K 6);
 
+fun with_typedef_threshold threshold f lthy =
+  lthy
+  |> Config.put typedef_threshold threshold
+  |> f
+  |> Config.put typedef_threshold (Config.get lthy typedef_threshold);
+
+fun with_typedef_threshold_yield threshold f lthy =
+  lthy
+  |> Config.put typedef_threshold threshold
+  |> f
+  ||> Config.put typedef_threshold (Config.get lthy typedef_threshold);
+
 val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
 val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
 
diff -r 737d424cbac9 -r 6489d85ecc98 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Sep 06 10:28:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Sep 06 11:21:21 2016 +0200
@@ -494,12 +494,6 @@
     fp_sugar
   end;
 
-fun inline_pre_bnfs f lthy =
-  lthy
-  |> Config.put typedef_threshold ~1
-  |> f
-  |> Config.put typedef_threshold (Config.get lthy typedef_threshold);
-
 fun bnf_kill_all_but nn bnf lthy =
   ((empty_comp_cache, empty_unfolds), lthy)
   |> kill_bnf I (live_of_bnf bnf - nn) bnf
@@ -567,7 +561,8 @@
 
     val lthy = lthy
       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
-      |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
+      |> with_typedef_threshold ~1
+        (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
       |> Local_Theory.close_target;
 
     val SOME fp_sugar = fp_sugar_of lthy T_name;
@@ -606,7 +601,8 @@
 
     val lthy = lthy
       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
-      |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
+      |> with_typedef_threshold ~1
+        (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
       |> Local_Theory.close_target;
 
     val SOME fp_sugar = fp_sugar_of lthy T_name;