diff -r 6c28d8ed2488 -r 4592a9118d0b src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jul 24 22:16:39 2015 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 24 22:19:36 2015 +0200
@@ -18,7 +18,6 @@
   val resolve_tac: Proof.context -> thm list -> int -> tactic
   val eresolve0_tac: thm list -> int -> tactic
   val eresolve_tac: Proof.context -> thm list -> int -> tactic
-  val forward0_tac: thm list -> int -> tactic
   val forward_tac: Proof.context -> thm list -> int -> tactic
   val dresolve0_tac: thm list -> int -> tactic
   val dresolve_tac: Proof.context -> thm list -> int -> tactic
@@ -26,7 +25,6 @@
   val rtac: thm -> int -> tactic
   val dtac: thm -> int -> tactic
   val etac: thm -> int -> tactic
-  val ftac: thm -> int -> tactic
   val ares_tac: Proof.context -> thm list -> int -> tactic
   val solve_tac: Proof.context -> thm list -> int -> tactic
   val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
@@ -131,7 +129,6 @@
 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
 
 (*Forward reasoning using destruction rules.*)
-fun forward0_tac rls = resolve0_tac (map make_elim rls) THEN' atac;
 fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
 
 (*Like forward_tac, but deletes the assumption after use.*)
@@ -142,7 +139,6 @@
 fun rtac rl =  resolve0_tac [rl];
 fun dtac rl = dresolve0_tac [rl];
 fun etac rl = eresolve0_tac [rl];
-fun ftac rl =  forward0_tac [rl];
 
 (*Use an assumption or some rules*)
 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;