# HG changeset patch
# User traytel
# Date 1375956045 -7200
# Node ID f8fca14c8cbd6d10f80059c7b1f11771c74b3fbd
# Parent  6c89225ddeba84dfe094af039185952b2037e0d3
tuned

diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Aug 07 23:20:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 12:00:45 2013 +0200
@@ -326,7 +326,7 @@
     val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
 
     val coalg_in_thms = map (fn i =>
-      coalg_def RS @{thm subst[of _ _ "%x. x"]} RS mk_conjunctN n i RS bspec) ks
+      coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
 
     val coalg_set_thmss =
       let
@@ -922,9 +922,9 @@
       |> Thm.close_derivation;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
-      (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct1 RS mk_conjunctN n i)) ks;
+      (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
     val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS
-      (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;
+      (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;
 
     val incl_lsbis_thms =
       let
@@ -1482,8 +1482,8 @@
         map (fn i => map (fn i' =>
           split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
             else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
-              (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
+              (2, @{thm sum_case_weak_cong} RS iffD1) RS
+              (mk_sum_casesN n i' RS iffD1))) ks) ks
       end;
 
     val set_Lev_thmsss =
@@ -1838,7 +1838,7 @@
       end;
 
     val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
-      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm));
+      (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm));
 
     val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
 
@@ -2005,7 +2005,7 @@
 
     val dtor_corec_unique_thms =
       split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm)
+        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
 
diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Aug 07 23:20:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 12:00:45 2013 +0200
@@ -1135,7 +1135,7 @@
 
     val ctor_fold_unique_thms =
       split_conj_thm (mk_conjIN n RS
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm))
+        (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
 
     val fold_ctor_thms =
       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
@@ -1296,7 +1296,7 @@
 
     val ctor_rec_unique_thms =
       split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS rec_unique_mor_thm)
+        (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
 
diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Aug 07 23:20:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 08 12:00:45 2013 +0200
@@ -245,7 +245,7 @@
           REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
       (set_map's ~~ alg_sets);
   in
-    (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) 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
@@ -372,7 +372,7 @@
             etac @{thm underS_I}, atac, atac]]))
           set_bds];
   in
-    (rtac (alg_def RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
+    (rtac (alg_def RS iffD2) THEN'
     CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1
   end;