diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/TLA/TLA.ML	Thu May 30 10:12:52 2002 +0200
@@ -999,8 +999,6 @@
  by (etac STL4E 1); 
  by (rtac DmdImpl 1);
  by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1);
- by (rtac nat_less_cases 1);
- by Auto_tac;
 by (rtac (temp_use wf_box_dmd_decrease) 1);
 by (auto_tac (temp_css addSEs2 [STL4E,DmdImplE]));
 qed "nat_box_dmd_decrease";