yields ill-typed ATP/metis proofs -- raus!

--- a/src/HOL/Predicate.thy	Thu Jun 24 21:00:37 2010 +0200
+++ b/src/HOL/Predicate.thy	Thu Jun 24 21:01:13 2010 +0200
@@ -645,7 +645,7 @@
 lemma "f () = False \<or> f () = True"
 by simp
 
-lemma closure_of_bool_cases:
+lemma closure_of_bool_cases [no_atp]:
 assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
 assumes "f = (%u. True) \<Longrightarrow> P f"
 shows "P f"