src/HOL/ex/MT.ML

--- a/src/HOL/ex/MT.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/ex/MT.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -639,7 +639,7 @@
 by (dtac elab_fix_elim 1);
 by (safe_tac HOL_cs);
 (*Do a single unfolding of cl*)
-by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
+by ((ftac ssubst 1) THEN (assume_tac 2));
 by (rtac hasty_rel_clos_coind 1);
 by (etac elab_fn 1);
 by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);