Got rid of some slow deepen_tac calls

--- a/src/HOL/IMP/Hoare.ML	Thu Nov 20 10:54:04 1997 +0100
+++ b/src/HOL/IMP/Hoare.ML	Thu Nov 20 10:55:27 1997 +0100
@@ -95,7 +95,7 @@
 by (com.induct_tac "c" 1);
 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
-by (deepen_tac (claset() addIs [hoare.conseq]) 0 1);
+by (blast_tac (claset() addIs [hoare.conseq]) 1);
 by Safe_tac;
 by (rtac hoare.conseq 1);
   by (etac thin_rl 1);

--- a/src/HOL/IMP/Natural.ML	Thu Nov 20 10:54:04 1997 +0100
+++ b/src/HOL/IMP/Natural.ML	Thu Nov 20 10:55:27 1997 +0100
@@ -20,5 +20,6 @@
 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
 by (etac evalc.induct 1);
 by (thin_tac "<?c,s2> -c-> s1" 7);
-by (ALLGOALS (deepen_tac (claset() addEs [evalc_WHILE_case]) 4));
+(*blast_tac needs Unify.search_bound, trace_bound := 40*)
+by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
 qed_spec_mp "com_det";