src/HOL/BNF/Tools/bnf_gfp.ML
changeset 53289 5e0623448bdb
parent 53288 050d0bc9afa5
child 53290 b6c3be868217
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:39:46 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:56:39 2013 +0200
     1.3 @@ -2462,7 +2462,7 @@
     1.4          val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
     1.5          val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
     1.6          val set_nat_tacss =
     1.7 -          map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss);
     1.8 +          map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss);
     1.9  
    1.10          val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order));
    1.11          val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite));
    1.12 @@ -2701,10 +2701,10 @@
    1.13            in
    1.14              map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
    1.15                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
    1.16 -              fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
    1.17 +              fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
    1.18                Goal.prove_sorry lthy [] [] goal
    1.19                  (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
    1.20 -                  dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
    1.21 +                  dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
    1.22                |> Thm.close_derivation)
    1.23              ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
    1.24                dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss