# HG changeset patch
# User traytel
# Date 1394400424 -3600
# Node ID 508836bbfed4c1740a042e2fd4fc747303673368
# Parent  158dc03db8be4bdc59544fcf6d72f8782398cd8c
more careful unfolding of internal constants

diff -r 158dc03db8be -r 508836bbfed4 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 21:40:41 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 22:27:04 2014 +0100
@@ -765,9 +765,9 @@
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
 
-    val map_unfolds = #map_unfolds unfold_set;
+    val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
     val set_unfoldss = #set_unfoldss unfold_set;
-    val rel_unfolds = #rel_unfolds unfold_set;
+    val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
 
     val expand_maps = expand_id_bnf_comp_def o
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);