diff -r 4a4f6ad607a1 -r fdf4638bf726 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Mon Dec 28 17:03:47 1998 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Mon Jan 04 15:07:47 1999 +0100
@@ -110,7 +110,6 @@
 Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
-by (blast_tac (claset() addDs [add_lessD1]) 1);
 qed "liftn_lift";
 Addsimps [liftn_lift];