--- a/src/HOL/Lambda/Eta.ML Mon Apr 21 10:12:40 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML Mon Apr 21 10:13:47 1997 +0200
@@ -151,8 +151,8 @@
by (etac beta.induct 1);
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
addss !simpset) 1);
-by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 6 1);
-by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 6 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
(*23 seconds?*)
DelIffs dB.distinct;
Addsimps dB.distinct;