--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 14:09:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 14:15:29 2010 +0200
@@ -532,6 +532,8 @@
| (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, @{const False}) => true
+ | (false, @{const True}) => true
| _ => false
in do_formula true end