diff -r e5128a9c4311 -r 565a20b22f09 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 26 10:10:38 2014 +0100
@@ -16,7 +16,7 @@
   val mk_bd_card_order_tac: thm list -> tactic
   val mk_bd_limit_tac: int -> thm -> tactic
   val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic
+  val mk_copy_alg_tac: Proof.context -> thm list list -> thm list -> thm -> thm -> thm -> tactic
   val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
   val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
     thm list -> thm list -> thm list -> tactic
@@ -216,7 +216,8 @@
     val copy_str_tac =
       CONJ_WRAP' (fn (thms, thm) =>
         EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
-          rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
+          rtac equalityD1, etac @{thm bij_betw_imageE},
+          REPEAT_DETERM_N 2 o rtac @{thm ssubst_mem[OF o_apply]}, rtac imageI, etac thm,
           REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
@@ -224,7 +225,7 @@
     stac alg_def THEN' copy_str_tac) 1
   end;
 
-fun mk_copy_alg_tac set_maps alg_sets mor_def iso_alt copy_str =
+fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str =
   let
     val n = length alg_sets;
     val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
@@ -234,12 +235,11 @@
         rtac equalityD1, etac @{thm bij_betw_imageE}];
     val mor_tac =
       CONJ_WRAP' (fn (thms, thm) =>
-        EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
-          REPEAT_DETERM_N n o set_tac thms])
+        EVERY' [rtac ballI, etac CollectE, SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
+          etac @{thm inverE}, etac thm, REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
-    (rtac (iso_alt RS iffD2) THEN'
-    etac copy_str THEN' REPEAT_DETERM o atac THEN'
+    (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN'
     rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
     CONJ_WRAP' (K atac) alg_sets) 1
   end;