# HG changeset patch
# User paulson
# Date 861610427 -7200
# Node ID 2a311f90747cd4cd195fb286a4497049ece092e9
# Parent  84df3b150b67c0d7bdc2782aa361de25988163c5
Now faster without calling Blast.depth_tac

diff -r 84df3b150b67 -r 2a311f90747c src/HOL/Lambda/Eta.ML
--- 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;