src/HOL/MiniML/Instance.ML
changeset 7499 23e090051cb8
parent 5983 79e301a6a51b
--- a/src/HOL/MiniML/Instance.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/MiniML/Instance.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -127,7 +127,7 @@
 by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); 
 by (rtac iffI 1); 
 by (etac exE 1); 
-by (forward_tac [bound_scheme_inst_type] 1);
+by (ftac bound_scheme_inst_type 1);
 by (etac exE 1);
 by (rtac exI 1);
 by (rtac mk_scheme_injective 1);