# HG changeset patch
# User blanchet
# Date 1355323127 -3600
# Node ID 8665ec681e472e2238dd5ca121ca4c40b6703c72
# Parent  bd9a0028b063939a04fe1e35eec06d17f9fc2a9f
further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"

diff -r bd9a0028b063 -r 8665ec681e47 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 15:25:17 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 15:38:47 2012 +0100
@@ -220,8 +220,8 @@
     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
         is_boring_prop Ts t andalso is_boring_prop Ts u
-      | is_boring_prop Ts (Const (@{const_name all}, _) $ (Abs (_, T, t)) $ u) =
-        is_boring_prop (T :: Ts) t andalso is_boring_prop (T :: Ts) u
+      | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
+        is_boring_prop (T :: Ts) t
       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
         is_boring_prop Ts (t $ eta_expand Ts u 1)
       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =