# HG changeset patch
# User wenzelm
# Date 1437769746 -7200
# Node ID ee811a49c8f6a8e56dd8be4f242f36a85c2ab0d2
# Parent  2164e7b47454cd04da1f9c326dc1bfb4a4f35bd2
eliminated alias;

diff -r 2164e7b47454 -r ee811a49c8f6 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jul 24 22:29:06 2015 +0200
@@ -212,7 +212,7 @@
               EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
                 etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
                 rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
-                ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
+                forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
                 rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
                 REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
             (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
@@ -418,7 +418,7 @@
   end;
 
 fun mk_length_Lev'_tac ctxt length_Lev =
-  EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1;
+  EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1;
 
 fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
   let
@@ -720,7 +720,7 @@
   let
     val n = length Rep_injects;
   in
-    EVERY' [rtac ctxt rev_mp, ftac ctxt (bis_def RS iffD1),
+    EVERY' [rtac ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1],
       REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
       rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
       rtac ctxt bis_Gr, rtac ctxt tcoalg,
diff -r 2164e7b47454 -r ee811a49c8f6 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jul 24 22:29:06 2015 +0200
@@ -340,7 +340,8 @@
       CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
       EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
-        rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
+        rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
+        rtac ctxt (str_init_def RS @{thm ssubst_mem}),
         etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
           rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
           assume_tac ctxt]];
diff -r 2164e7b47454 -r ee811a49c8f6 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jul 24 22:29:06 2015 +0200
@@ -57,7 +57,6 @@
   val rtac: Proof.context -> thm -> int -> tactic
   val etac: Proof.context -> thm -> int -> tactic
   val dtac: Proof.context -> thm -> int -> tactic
-  val ftac: Proof.context -> thm -> int -> tactic
 
   val list_all_free: term list -> term -> term
   val list_exists_free: term list -> term -> term
@@ -281,6 +280,5 @@
 fun rtac ctxt thm = resolve_tac ctxt [thm];
 fun etac ctxt thm = eresolve_tac ctxt [thm];
 fun dtac ctxt thm = dresolve_tac ctxt [thm];
-fun ftac ctxt thm = forward_tac ctxt [thm];
 
 end;