src/HOL/Hoare/Arith2.ML

--- a/src/HOL/Hoare/Arith2.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -36,7 +36,7 @@
 (*** gcd ***)
 
 Goalw [gcd_def] "0<n ==> n = gcd n n";
-by (forward_tac [cd_nnn] 1);
+by (ftac cd_nnn 1);
 by (rtac (select_equality RS sym) 1);
 by (blast_tac (claset() addDs [cd_le]) 1);
 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);