src/HOL/Auth/WooLam.ML

--- a/src/HOL/Auth/WooLam.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/Auth/WooLam.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -39,7 +39,7 @@
 (*For proving the easier theorems about X ~: parts (spies evs) *)
 fun parts_induct_tac i = 
     etac woolam.induct i  THEN 
-    forward_tac [WL4_parts_spies] (i+5)  THEN
+    ftac WL4_parts_spies (i+5)  THEN
     prove_simple_subgoals_tac 1;