diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -2733,7 +2733,7 @@
 prefer 2
 apply(drule minusinfinity)
 apply assumption+
-apply(fastsimp)
+apply(fastforce)
 apply clarsimp
 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
 apply(frule_tac x = x and z=z in decr_lemma)
@@ -2741,7 +2741,7 @@
 prefer 2
 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
 prefer 2 apply arith
- apply fastsimp
+ apply fastforce
 apply(drule (1)  periodic_finite_ex)
 apply blast
 apply(blast dest:decr_mult_lemma)