diff -r 340df9f3491f -r 22f665a2e91c src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -81,7 +81,7 @@
   "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
 apply (induct xs arbitrary: f vs)
  apply simp
-apply fastsimp
+apply fastforce
 done
 
 lemma map_upds_distinct [simp]: