# HG changeset patch
# User traytel
# Date 1575936399 -3600
# Node ID 4765fec434140aae6a21512e365fd19b60bb67ca
# Parent  308baf6b450a082ed7df31a81dab2ef549712de0
unfold intermediate (internal) pred definitions

diff -r 308baf6b450a -r 4765fec43414 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Dec 09 16:37:26 2019 +0000
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Dec 10 01:06:39 2019 +0100
@@ -21,7 +21,8 @@
   type unfold_set =
     {map_unfolds: thm list,
      set_unfoldss: thm list list,
-     rel_unfolds: thm list}
+     rel_unfolds: thm list,
+     pred_unfolds: thm list}
 
   val empty_comp_cache: comp_cache
   val empty_unfolds: unfold_set
@@ -124,23 +125,25 @@
 type unfold_set = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
-  rel_unfolds: thm list
+  rel_unfolds: thm list,
+  pred_unfolds: thm list
 };
 
 val empty_comp_cache = Typtab.empty;
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], pred_unfolds = []};
 
 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
 fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
 
-fun add_to_unfolds map sets rel
-  {map_unfolds, set_unfoldss, rel_unfolds} =
+fun add_to_unfolds map sets rel pred
+  {map_unfolds, set_unfoldss, rel_unfolds, pred_unfolds} =
   {map_unfolds = add_to_thms map_unfolds map,
     set_unfoldss = adds_to_thms set_unfoldss sets,
-    rel_unfolds = add_to_thms rel_unfolds rel};
+    rel_unfolds = add_to_thms rel_unfolds rel,
+    pred_unfolds = add_to_thms pred_unfolds pred};
 
 fun add_bnf_to_unfolds bnf =
-  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
+  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf) (pred_def_of_bnf bnf);
 
 val bdTN = "bdT";
 
@@ -955,7 +958,8 @@
         (((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel), SOME bnf_pred) lthy;
 
     val unfolds = @{thm id_bnf_apply} ::
-      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
+      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @
+       #rel_unfolds unfold_set @ #pred_unfolds unfold_set);
 
     val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
 
diff -r 308baf6b450a -r 4765fec43414 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Mon Dec 09 16:37:26 2019 +0000
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Dec 10 01:06:39 2019 +0100
@@ -91,7 +91,7 @@
 
     val _ = (case alphas of [] => error "No live variables" | _ => ());
 
-    val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds;
+    val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds @ #pred_unfolds unfolds;
 
     (* number of live variables *)
     val lives = length alphas;