Some tidying. This brittle proof depends upon
AddSEs [less_SucE];

--- a/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:23:13 1996 +0200
+++ b/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:32:16 1996 +0200
@@ -11,4 +11,6 @@
 writeln"Root file for HOL/MiniML";
 Unify.trace_bound := 20;
 
+AddSEs [less_SucE];
+
 time_use_thy "I";

--- a/src/HOL/MiniML/W.ML	Tue Aug 20 12:23:13 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Tue Aug 20 12:32:16 1996 +0200
@@ -132,26 +132,30 @@
      [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
     1);
 by (etac (sym RS mgu_new) 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,
-   new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
-   new_tv_subst_le,new_tv_le]) 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] addIs
-     [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
-        addss (!simpset)) 1);
+by (best_tac (HOL_cs addDs [W_var_geD] 
+	             addIs [new_tv_subst_te,new_tv_list_le,
+			    new_tv_subst_tel,
+			    lessI RS less_imp_le RS new_tv_le,
+			    lessI RS less_imp_le RS new_tv_subst_le,
+			    new_tv_le]) 1);
+by (fast_tac (HOL_cs addDs [W_var_geD] 
+	             addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
+		     addss (!simpset)) 1);
 by (rtac (lessI RS new_tv_subst_var) 1);
 by (etac (sym RS mgu_new) 1);
-by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
-   addDs [W_var_geD] addIs
-   [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS
-   new_tv_subst_le,new_tv_le] addss !simpset) 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] addIs
-     [new_tv_list_le,new_tv_subst_tel,new_tv_le]
-     addss (!simpset)) 1);
+by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
+                     addDs [W_var_geD]
+		     addIs [new_tv_list_le,
+			    new_tv_subst_tel,
+			    lessI RS less_imp_le RS new_tv_subst_le,
+			    new_tv_le] 
+		     addss !simpset) 1);
+by (fast_tac (HOL_cs addDs [W_var_geD] 
+	             addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
+                     addss (!simpset)) 1);
 qed_spec_mp "new_tv_W";
 
 
-AddSEs [less_SucE];
-
 goal thy
      "!n a s t m v. W e a n = Ok (s,t,m) -->            \
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";