Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made tactic more robust
authortraytel
Wed, 06 Aug 2014 10:20:50 +0200
changeset 57801 4adfa833072b
parent 57799 2e9d65505454
child 57802 9c065009cd8a
made tactic more robust
src/HOL/Tools/BNF/bnf_fp_n2m.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 08:18:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 10:20:50 2014 +0200
@@ -429,10 +429,11 @@
               rewrite_comp_comp)
           type_definitions bnfs);
 
-        fun mk_Rep_o_Abs thm = thm RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp;
+        fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs})
+          |> (fn thm => [thm, thm RS rewrite_comp_comp]);
 
-        val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions;
-        val Rep_o_Abss = map mk_Rep_o_Abs type_definitions;
+        val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions;
+        val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
 
         fun tac {context = ctxt, prems = _} =
           unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,
isabelle