# HG changeset patch
# User traytel
# Date 1375966099 -7200
# Node ID fe4c2418f06947f3eeabab427b883b6f64d9aea3
# Parent  41ebc19276eacf2b4d8ed68ecf7b565b319828c1
tuned tactic;

diff -r 41ebc19276ea -r fe4c2418f069 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 14:48:19 2013 +0200
@@ -2254,7 +2254,7 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
+              (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps)
               |> Thm.close_derivation
           end;
 
diff -r 41ebc19276ea -r fe4c2418f069 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 08 14:48:19 2013 +0200
@@ -1114,9 +1114,9 @@
            rtac conjI, rtac refl, rtac refl]) ks]) 1
   end
 
-fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
   rtac unfold_unique 1 THEN
-  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
   ALLGOALS (etac sym);
 
 fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
diff -r 41ebc19276ea -r fe4c2418f069 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 14:48:19 2013 +0200
@@ -1133,8 +1133,8 @@
         `split_conj_thm unique_mor
       end;
 
-    val ctor_fold_unique_thms =
-      split_conj_thm (mk_conjIN n RS
+    val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
+      `split_conj_thm (mk_conjIN n RS
         (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
 
     val fold_ctor_thms =
@@ -1472,7 +1472,7 @@
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
+              (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps)
               |> Thm.close_derivation;
           in
             `split_conj_thm unique
diff -r 41ebc19276ea -r fe4c2418f069 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 08 14:48:19 2013 +0200
@@ -42,7 +42,7 @@
   val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
   val mk_map_id_tac: thm list -> thm -> tactic
   val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
-  val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
+  val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
   val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
@@ -584,19 +584,10 @@
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
     rtac sym, rtac o_apply] 1;
 
-fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
-  let
-    val n = length map_cong0s;
-    fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest},
-      rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
-      rtac (cong RS arg_cong),
-      REPEAT_DETERM_N m o rtac refl,
-      REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
-  in
-    EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
-      CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
-      CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
-  end;
+fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} =
+  rtac fold_unique 1 THEN
+  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
+  ALLGOALS atac;
 
 fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
   rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;