# HG changeset patch
# User traytel
# Date 1348220695 -7200
# Node ID 02eb071529986df6594d1fe3735d6c07c8a7e943
# Parent  7e7ac495611782036437cc6fb6ac99da92669adc
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;

diff -r 7e7ac4956117 -r 02eb07152998 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
@@ -56,7 +56,6 @@
 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
 val ordIso_transitive = @{thm ordIso_transitive};
 val ordLeq_csum2 = @{thm ordLeq_csum2};
-val set_mp = @{thm set_mp};
 val subset_UNIV = @{thm subset_UNIV};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};
diff -r 7e7ac4956117 -r 02eb07152998 src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
@@ -33,8 +33,6 @@
 open BNF_Util
 open BNF_Tactics
 
-val set_mp = @{thm set_mp};
-
 fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
 fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
@@ -75,9 +73,9 @@
     else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac subsetI,
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
         REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
           REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
@@ -89,7 +87,7 @@
           REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
           stac @{thm fst_conv}, atac]) set_naturals,
         rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
         REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
@@ -99,7 +97,7 @@
         rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
         rtac @{thm relcompI}, rtac @{thm converseI},
         REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
+          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym,
           etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
           REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
   end;
@@ -128,11 +126,11 @@
     else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
+          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
           rtac map_cong, REPEAT_DETERM_N n o rtac thm,
           rtac (map_comp RS sym), rtac CollectI,
           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
@@ -155,32 +153,32 @@
     else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
         REPEAT_DETERM_N n o rtac @{thm fst_fstO},
         in_tac @{thm fstO_in},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
         REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
           rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
           etac set_mp, atac],
         in_tac @{thm fstO_in},
         rtac @{thm relcompI}, rtac @{thm converseI},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
         REPEAT_DETERM_N n o rtac o_apply,
         in_tac @{thm sndO_in},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
         REPEAT_DETERM_N n o rtac @{thm snd_sndO},
         in_tac @{thm sndO_in},
         rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [exE, conjE],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
         CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
@@ -188,7 +186,7 @@
         REPEAT_DETERM o eresolve_tac [bexE, conjE],
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
+          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
           rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   end;
diff -r 7e7ac4956117 -r 02eb07152998 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
@@ -129,25 +129,20 @@
 open BNF_FP
 open BNF_GFP_Util
 
-val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
-val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]};
+val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
 val nat_induct = @{thm nat_induct};
 val o_apply_trans_sym = o_apply RS trans RS sym;
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
 val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
   @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
-val subst_id = @{thm subst[of _ _ "%x. x"]};
 val sum_case_weak_cong = @{thm sum_case_weak_cong};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 
 fun mk_coalg_set_tac coalg_def =
-  dtac (coalg_def RS subst_id) 1 THEN
+  dtac (coalg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac conjE 1) THEN
   EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
@@ -291,7 +286,7 @@
         dtac (rel_O_Gr RS equalityD1 RS set_mp),
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
-        REPEAT_DETERM o dtac Pair_eq_subst_id,
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE,
         hyp_subst_tac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -319,7 +314,7 @@
   end;
 
 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
-  EVERY' [stac bis_rel, dtac (bis_rel RS subst_id),
+  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
       rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
@@ -333,7 +328,7 @@
         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
 
 fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
-  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id),
+  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_O) =>
@@ -343,7 +338,7 @@
         REPEAT_DETERM_N (length rel_congs) o rtac refl,
         rtac rel_O,
         etac @{thm relcompE},
-        REPEAT_DETERM o dtac Pair_eq_subst_id,
+        REPEAT_DETERM o dtac Pair_eqD,
         etac conjE, hyp_subst_tac,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
@@ -391,17 +386,17 @@
     rtac (mk_nth_conv n i)] 1;
 
 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
-  EVERY' [rtac (@{thm equiv_def} RS ssubst_id),
+  EVERY' [rtac (@{thm equiv_def} RS iffD2),
 
-    rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id),
+    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
     rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
     rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
 
-    rtac conjI, rtac (@{thm sym_def} RS ssubst_id),
+    rtac conjI, rtac (@{thm sym_def} RS iffD2),
     rtac allI, rtac allI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
 
-    rtac (@{thm trans_def} RS ssubst_id),
+    rtac (@{thm trans_def} RS iffD2),
     rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
     etac @{thm relcompI}, atac] 1;
@@ -535,7 +530,7 @@
       hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
-        [rtac (mk_UnIN n i), dtac (def RS subst_id),
+        [rtac (mk_UnIN n i), dtac (def RS iffD1),
         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
         CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
@@ -547,9 +542,9 @@
 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
   EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
     REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-    dtac Pair_eq_subst_id,
+    dtac Pair_eqD,
     etac conjE, hyp_subst_tac,
-    dtac (isNode_def RS subst_id),
+    dtac (isNode_def RS iffD1),
     REPEAT_DETERM o eresolve_tac [exE, conjE],
     rtac (equalityD2 RS set_mp),
     rtac (strT_def RS arg_cong RS trans),
@@ -573,8 +568,8 @@
           rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
         else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
-          dtac conjunct2, dtac Pair_eq_subst_id, etac conjE,
-          hyp_subst_tac, dtac (isNode_def RS subst_id),
+          dtac conjunct2, dtac Pair_eqD, etac conjE,
+          hyp_subst_tac, dtac (isNode_def RS iffD1),
           REPEAT_DETERM o eresolve_tac [exE, conjE],
           rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
       (ks ~~ (carT_defs ~~ isNode_defs));
@@ -719,8 +714,8 @@
       CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
         EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
           dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
-          rtac (rv_Nil RS arg_cong RS ssubst_id),
-          rtac (mk_sum_casesN n i RS ssubst_id),
+          rtac (rv_Nil RS arg_cong RS iffD2),
+          rtac (mk_sum_casesN n i RS iffD2),
           CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
       (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
       REPEAT_DETERM o rtac allI,
@@ -729,8 +724,8 @@
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, coalg_set)) =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              rtac (rv_Cons RS arg_cong RS ssubst_id),
-              rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id),
+              rtac (rv_Cons RS arg_cong RS iffD2),
+              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
               etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
               dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
               etac coalg_set, atac])
@@ -802,7 +797,7 @@
                 hyp_subst_tac,
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
                   (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                    dtac list_inject_subst_id THEN' etac conjE THEN'
+                    dtac list_inject_iffD1 THEN' etac conjE THEN'
                     (if k = i'
                     then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
                     else etac (mk_InN_not_InM i' k RS notE)))
@@ -822,10 +817,10 @@
                 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
                   REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                  dtac list_inject_subst_id THEN' etac conjE THEN'
+                  dtac list_inject_iffD1 THEN' etac conjE THEN'
                   (if k = i
                   then EVERY' [dtac (mk_InN_inject n i),
-                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                     atac, atac, hyp_subst_tac] THEN'
                     CONJ_WRAP' (fn i'' =>
                       EVERY' [rtac impI, dtac (sym RS trans),
@@ -957,7 +952,7 @@
           rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
         rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
-          DETERM o EVERY' [rtac trans, rtac o_apply, rtac ssubst, rtac @{thm Pair_eq}, rtac conjI,
+          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
             rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
@@ -965,9 +960,9 @@
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac list_inject_subst_id, etac conjE,
+                dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
@@ -980,9 +975,9 @@
             dtac (Lev_Suc RS equalityD1 RS set_mp),
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac list_inject_subst_id, etac conjE,
+                dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   atac, atac, hyp_subst_tac, atac]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
@@ -1067,7 +1062,7 @@
     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
-  EVERY' [rtac ssubst_id, rtac mor_UNIV,
+  EVERY' [rtac iffD2, rtac mor_UNIV,
     CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
         rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
@@ -1082,7 +1077,7 @@
   let
     val n = length Rep_injects;
   in
-    EVERY' [rtac rev_mp, ftac (bis_def RS subst_id),
+    EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
       REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
       rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
       rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
@@ -1456,7 +1451,7 @@
 
 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   mor_unique pick_cols hset_defs =
-  EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI,
+  EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
     REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
     rtac box_equals, rtac mor_unique,
     rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
diff -r 7e7ac4956117 -r 02eb07152998 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
@@ -86,15 +86,12 @@
 val id_apply = @{thm id_apply};
 val meta_mp = @{thm meta_mp};
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
 val subset_UNIV = @{thm subset_UNIV};
 val subset_trans = @{thm subset_trans};
-val subst_id = @{thm subst[of _ _ "\<lambda>x. x"]};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 
 fun mk_alg_set_tac alg_def =
-  dtac (alg_def RS subst_id) 1 THEN
+  dtac (alg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac conjE 1) THEN
   EVERY' [etac bspec, rtac CollectI] 1 THEN
   REPEAT_DETERM (etac conjI 1) THEN atac 1;
@@ -161,8 +158,8 @@
            (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
   in
     (stac mor_def THEN'
-    dtac (alg_def RS subst_id) THEN'
-    dtac (alg_def RS subst_id) THEN'
+    dtac (alg_def RS iffD1) THEN'
+    dtac (alg_def RS iffD1) THEN'
     REPEAT o etac conjE THEN'
     rtac conjI THEN'
     CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
@@ -281,7 +278,7 @@
     (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
     rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
     REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
-    CONJ_WRAP_GEN' (EVERY' [rtac ssubst, rtac @{thm Pair_eq}, rtac conjI]) minH_tac in_congs) 1
+    CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
   end;
 
 fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
diff -r 7e7ac4956117 -r 02eb07152998 src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 11:44:55 2012 +0200
@@ -121,6 +121,10 @@
 
   val ctrans: thm
   val o_apply: thm
+  val set_mp: thm
+  val set_rev_mp: thm
+  val Pair_eqD: thm
+  val Pair_eqI: thm
   val mk_sym: thm -> thm
   val mk_trans: thm -> thm -> thm
   val mk_unabs_def: int -> thm -> thm
@@ -518,6 +522,10 @@
 (*TODO: antiquote heavily used theorems once*)
 val ctrans = @{thm ordLeq_transitive};
 val o_apply = @{thm o_apply};
+val set_mp = @{thm set_mp};
+val set_rev_mp = @{thm set_rev_mp};
+val Pair_eqD = @{thm iffD1[OF Pair_eq]};
+val Pair_eqI = @{thm iffD2[OF Pair_eq]};
 
 fun mk_nthN 1 t 1 = t
   | mk_nthN _ t 1 = HOLogic.mk_fst t