src/HOL/Tools/BNF/bnf_comp.ML
changeset 56013 508836bbfed4
parent 56012 158dc03db8be
child 56016 8875cdcfc85b
equal deleted inserted replaced
56012:158dc03db8be 56013:508836bbfed4
   763 
   763 
   764     val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
   764     val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
   765       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
   765       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
   766       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
   766       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
   767 
   767 
   768     val map_unfolds = #map_unfolds unfold_set;
   768     val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
   769     val set_unfoldss = #set_unfoldss unfold_set;
   769     val set_unfoldss = #set_unfoldss unfold_set;
   770     val rel_unfolds = #rel_unfolds unfold_set;
   770     val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
   771 
   771 
   772     val expand_maps = expand_id_bnf_comp_def o
   772     val expand_maps = expand_id_bnf_comp_def o
   773       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
   773       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
   774     val expand_sets =
   774     val expand_sets =
   775       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
   775       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);