src/HOL/MiniML/W.ML

 by (eres_inst_tac [("x","v")] allE 1);
 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
 by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
 by (dtac W_var_geD 1);
 by (dtac W_var_geD 1);
-by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
+by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
     less_le_trans,less_not_refl2,subsetD]
   addEs [UnE] 
   addss simpset()) 1);
 by (Asm_full_simp_tac 1); 
 by (dtac (sym RS W_var_geD) 1);
 by (dtac (sym RS W_var_geD) 1);
-by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
+by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
     free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
     less_le_trans,subsetD]
   addEs [UnE]
   addss (simpset() setSolver unsafe_solver)) 1);

 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym,o_def]) 1);
 by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
 by (rtac (has_type_cl_sub RS spec) 1);
-by (forward_tac [new_tv_W] 1);
+by (ftac new_tv_W 1);
 by (assume_tac 1);
 by (dtac conjunct1 1);
 by (dtac conjunct1 1);
-by (forward_tac [new_tv_subst_scheme_list] 1);
+by (ftac new_tv_subst_scheme_list 1);
 by (rtac new_scheme_list_le 1);
 by (rtac W_var_ge 1);
 by (assume_tac 1);
 by (assume_tac 1);
 by (etac thin_rl 1);

 by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
 by (dres_inst_tac [("x","S2")] spec 2);
 by (dres_inst_tac [("x","t")] spec 2);
 by (dres_inst_tac [("x","n2")] spec 2);
 by (dres_inst_tac [("x","m2")] spec 2);
-by (forward_tac [new_tv_W] 2);
+by (ftac new_tv_W 2);
 by (assume_tac 2);
 by (dtac conjunct1 2);
 by (dtac conjunct1 2);
-by (forward_tac [new_tv_subst_scheme_list] 2);
+by (ftac new_tv_subst_scheme_list 2);
 by (rtac new_scheme_list_le 2);
 by (rtac W_var_ge 2);
 by (assume_tac 2);
 by (assume_tac 2);
 by (etac impE 2);

 by (subgoal_tac "na ~=ma" 2);
 by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
     new_tv_not_free_tv,new_tv_le]) 3);
 by (case_tac "na:free_tv Sa" 2);
 (* n1 ~: free_tv S1 *)
-by (forward_tac [not_free_impl_id] 3);
+by (ftac not_free_impl_id 3);
 by (Asm_simp_tac 3);
 (* na : free_tv Sa *)
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);

 by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
 (* na : dom Sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
 by (subgoal_tac "nb ~= ma" 2);
-by ((forward_tac [new_tv_W] 3) THEN (atac 3));
+by ((ftac new_tv_W 3) THEN (atac 3));
 by (etac conjE 3);
 by (dtac new_tv_subst_scheme_list 3);
 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
     (simpset() addsimps [cod_def,free_tv_subst])) 3);
 by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
 by (Simp_tac 2);  
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
 by (subgoal_tac "na ~= ma" 2);
-by ((forward_tac [new_tv_W] 3) THEN (atac 3));
+by ((ftac new_tv_W 3) THEN (atac 3));
 by (etac conjE 3);
 by (dtac (sym RS W_var_geD) 3);
 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv Sa" 2);
 (* case na ~: free_tv t - free_tv Sa *)

 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
 by (dres_inst_tac [("s","Some ?X")] sym 1);
 by (rtac eq_free_eq_subst_scheme_list 1);
 by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
-by ((forward_tac [new_tv_W] 2) THEN (atac 2));
+by ((ftac new_tv_W 2) THEN (atac 2));
 by (etac conjE 2);
 by (dtac new_tv_subst_scheme_list 2);
 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
 by (forw_inst_tac [("n","m")] new_tv_W 2  THEN  atac 2);
 by (etac conjE 2);

 by (rtac has_type_le_env 1);
 by (assume_tac 1);
 by (Simp_tac 1);
 by (rtac gen_bound_typ_instance 1);
 by (dtac mp 1);
-by (forward_tac [new_tv_compatible_W] 1);
+by (ftac new_tv_compatible_W 1);
 by (rtac sym 1);
 by (assume_tac 1);
 by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
 by (safe_tac HOL_cs);
 by (Asm_full_simp_tac 1);