# HG changeset patch
# User blanchet
# Date 1380747282 -7200
# Node ID 04715fecbda6224712ee73e59d5dda8b84fa6acf
# Parent  c931190b8c5c35e0dbbdfad1313221b4ff7ad1d9
strengthen top sort check

diff -r c931190b8c5c -r 04715fecbda6 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 02 19:49:31 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 02 22:54:42 2013 +0200
@@ -251,7 +251,7 @@
       | interest_of_prop Ts (@{const "==>"} $ t $ u) =
         combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
       | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
-        interest_of_prop (T :: Ts) t
+        if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
       | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
         interest_of_prop Ts (t $ eta_expand Ts u 1)
       | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =