diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -93,7 +93,7 @@
  by (dtac sym 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (hyp_subst_tac 1));
-by (forward_tac  [reachable_rename] 1);
+by (ftac reachable_rename 1);
 by (Asm_full_simp_tac 1);
 (* x is output *)
  by (etac exE 1);
@@ -102,10 +102,10 @@
  by (dtac sym 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (hyp_subst_tac 1));
-by (forward_tac  [reachable_rename] 1);
+by (ftac reachable_rename 1);
 by (Asm_full_simp_tac 1);
 (* x is internal *)
-by (forward_tac  [reachable_rename] 1);
+by (ftac reachable_rename 1);
 by Auto_tac;
 qed"rename_through_pmap";
 Addsplits [split_if]; Addcongs [if_weak_cong];