diff -r 5583261db33d -r fba734ba6894 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/MiniML/W.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -62,10 +62,6 @@
 by (rtac add_le_mono 1);
  by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [max_def]) 1);
-by (strip_tac 1);
-by (dtac not_leE 1);
-by (rtac less_or_eq_imp_le 1);
-by (Fast_tac 1);
 qed_spec_mp "new_tv_bound_typ_inst_sch";
 
 Addsimps [new_tv_bound_typ_inst_sch];