more careful unfolding of internal constants
authortraytel
Sun Mar 09 22:27:04 2014 +0100 (2014-03-09)
changeset 56013508836bbfed4
parent 56012 158dc03db8be
child 56014 aaa3f2365fc5
more careful unfolding of internal constants
src/HOL/Tools/BNF/bnf_comp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 21:40:41 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 22:27:04 2014 +0100
     1.3 @@ -765,9 +765,9 @@
     1.4        |> mk_Frees' "f" (map2 (curry op -->) As Bs)
     1.5        ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
     1.6  
     1.7 -    val map_unfolds = #map_unfolds unfold_set;
     1.8 +    val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
     1.9      val set_unfoldss = #set_unfoldss unfold_set;
    1.10 -    val rel_unfolds = #rel_unfolds unfold_set;
    1.11 +    val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
    1.12  
    1.13      val expand_maps = expand_id_bnf_comp_def o
    1.14        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);