--- 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");