diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -2613,7 +2613,7 @@
     and inequality: "u \<le> lx \<and> ux \<le> l'"
     by (cases "approx prec x vs", auto,
       cases "approx prec a vs", auto,
-      cases "approx prec b vs", auto, blast)
+      cases "approx prec b vs", auto)
   from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
   show ?case by auto
 qed
@@ -2902,7 +2902,7 @@
                (Mult (Inverse (Num (Float (int k) 0)))
                      (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
                            (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
-      by (auto elim!: lift_bin) blast
+      by (auto elim!: lift_bin)
 
     from bnd_c `x < length xs`
     have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (c,c)])"