src/HOL/BNF/Tools/bnf_comp.ML
changeset 49630 9f6ca87ab405
parent 49586 d5e342ffe91e
child 49669 620fa6272c48
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 08:59:54 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 09:17:30 2012 +0200
     1.3 @@ -158,17 +158,9 @@
     1.4      (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     1.5      val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
     1.6  
     1.7 -    fun map_id_tac {context = ctxt, ...} =
     1.8 -      let
     1.9 -        (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
    1.10 -          rules*)
    1.11 -        val thms = (map map_id_of_bnf inners
    1.12 -          |> map (`(Term.size_of_term o Thm.prop_of))
    1.13 -          |> sort (rev_order o int_ord o pairself fst)
    1.14 -          |> map snd) @ [map_id_of_bnf outer];
    1.15 -      in
    1.16 -        (EVERY' (map (fn thm => subst_tac ctxt NONE [thm]) thms) THEN' rtac refl) 1
    1.17 -      end;
    1.18 +    fun map_id_tac _ =
    1.19 +      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong_of_bnf outer)
    1.20 +        (map map_id_of_bnf inners);
    1.21  
    1.22      fun map_comp_tac _ =
    1.23        mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)