--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Wed Oct 28 12:29:00 2009 +0100
@@ -45,7 +45,7 @@
unfolding mem_def[symmetric, of _ a2]
apply auto
unfolding mem_def
- apply auto
+ apply fastsimp
done
qed