# HG changeset patch
# User blanchet
# Date 1282306529 -7200
# Node ID 405a527252c90c895c2c67825a573601b29a8a01
# Parent  5266689abbc1d90e561a89728a113c3088c54324
improve "x = A | x = B | x = C"-style fact discovery

diff -r 5266689abbc1 -r 405a527252c9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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