# HG changeset patch
# User blanchet
# Date 1277406073 -7200
# Node ID a62f742f1d580b11f6a75d55e988153c74bf5c77
# Parent  6a7a9261b9ad6ed8ec6137144d63dd636762bb56
yields ill-typed ATP/metis proofs -- raus!

diff -r 6a7a9261b9ad -r a62f742f1d58 src/HOL/Predicate.thy
--- 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"