made tactic more robust
authortraytel
Wed Aug 06 10:20:50 2014 +0200 (2014-08-06)
changeset 578014adfa833072b
parent 57799 2e9d65505454
child 57802 9c065009cd8a
made tactic more robust
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 08:18:35 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 10:20:50 2014 +0200
     1.3 @@ -429,10 +429,11 @@
     1.4                rewrite_comp_comp)
     1.5            type_definitions bnfs);
     1.6  
     1.7 -        fun mk_Rep_o_Abs thm = thm RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp;
     1.8 +        fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs})
     1.9 +          |> (fn thm => [thm, thm RS rewrite_comp_comp]);
    1.10  
    1.11 -        val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions;
    1.12 -        val Rep_o_Abss = map mk_Rep_o_Abs type_definitions;
    1.13 +        val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions;
    1.14 +        val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
    1.15  
    1.16          fun tac {context = ctxt, prems = _} =
    1.17            unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,