# HG changeset patch
# User blanchet
# Date 1282146792 -7200
# Node ID ae6bb801e583e63fe51a6e34b5805782473a85e1
# Parent  7400530ab1d039e7c18ebb6845552ee1f40e0643
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")

diff -r 7400530ab1d0 -r ae6bb801e583 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 17:23:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 17:53:12 2010 +0200
@@ -119,7 +119,8 @@
           else
             I)
     and do_term_or_formula T =
-     if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE else do_term
+      if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+      else do_term
     and do_formula pos t =
       case t of
         Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
@@ -532,15 +533,17 @@
     too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
   | too_general_equality _ = false
 
-fun has_typed_var tycons = exists_subterm
-  (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
+fun has_bound_or_var_of_type tycons =
+  exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
+                   | Abs (_, Type (s, _), _) => member (op =) tycons s
+                   | _ => false)
 
 (* Facts are forbidden to contain variables of these types. The typical reason
    is that they lead to unsoundness. Note that "unit" satisfies numerous
    equations like "?x = ()". The resulting clauses will have no type constraint,
    yielding false proofs. Even "bool" leads to many unsound proofs, though only
    for higher-order problems. *)
-val dangerous_types = [@{type_name unit}, @{type_name bool}];
+val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
 
 (* Facts containing variables of type "unit" or "bool" or of the form
    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
@@ -548,7 +551,7 @@
 fun is_dangerous_term _ @{prop True} = true
   | is_dangerous_term full_types t =
     not full_types andalso
-    (has_typed_var dangerous_types t orelse
+    (has_bound_or_var_of_type dangerous_types t orelse
      forall too_general_equality (HOLogic.disjuncts (strip_Trueprop_and_all t)))
 
 fun relevant_facts full_types relevance_threshold relevance_convergence