# HG changeset patch
# User blanchet
# Date 1282314171 -7200
# Node ID 4e1d828ee514f1bffcf2ed97008576518f622127
# Parent  61672fa2983a082ffcb7065b4f6f64622712a24c
improve "x = A | x = B | x = C"-style axiom detection

diff -r 61672fa2983a -r 4e1d828ee514 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 15:56:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 16:22:51 2010 +0200
@@ -516,7 +516,7 @@
       too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
     fun do_formula pos t =
       case (pos, t) of
-        (_, @{const Trueprop} $ t) => do_formula pos t
+        (_, @{const Trueprop} $ t1) => do_formula pos t1
       | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
         do_formula pos t'
       | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
@@ -532,8 +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
+      | (_, @{const False}) => true
+      | (_, @{const True}) => true
       | _ => false
   in do_formula true end