src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54040 04715fecbda6
parent 53815 e8aa538e959e
child 54076 5337fd7d53c9
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 02 19:49:31 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 02 22:54:42 2013 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4        | interest_of_prop Ts (@{const "==>"} $ t $ u) =
     1.5          combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
     1.6        | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
     1.7 -        interest_of_prop (T :: Ts) t
     1.8 +        if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
     1.9        | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
    1.10          interest_of_prop Ts (t $ eta_expand Ts u 1)
    1.11        | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =