--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Aug 22 08:12:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Aug 22 08:26:09 2010 +0200
@@ -443,15 +443,13 @@
(* Unwanted equalities are those between a (bound or schematic) variable that
does not properly occur in the second operand. *)
-fun too_general_eqterms (Var z) t =
- not (exists_subterm (fn Var z' => z = z' | _ => false) t)
- | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j))
- | too_general_eqterms _ _ = false
-
val is_exhaustive_finite =
let
- fun do_equals t1 t2 =
- too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
+ fun is_bad_equal (Var z) t =
+ not (exists_subterm (fn Var z' => z = z' | _ => false) t)
+ | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
+ | is_bad_equal _ _ = false
+ fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
fun do_formula pos t =
case (pos, t) of
(_, @{const Trueprop} $ t1) => do_formula pos t1
@@ -462,16 +460,16 @@
| (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
do_formula pos t'
| (_, @{const "==>"} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso do_formula pos t2
+ do_formula (not pos) t1 andalso
+ (t2 = @{prop False} orelse do_formula pos t2)
| (_, @{const "op -->"} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso do_formula pos t2
+ do_formula (not pos) t1 andalso
+ (t2 = @{const False} orelse do_formula pos t2)
| (_, @{const Not} $ t1) => do_formula (not pos) t1
| (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (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
- | (_, @{const False}) => true
- | (_, @{const True}) => true
| _ => false
in do_formula true end