# HG changeset patch
# User blanchet
# Date 1311846225 -7200
# Node ID a2aa341bc6581da87ceb0dc1ccd1fe1aaf0d7ce5
# Parent  5784609715172f071e26cd6bd59bd6e255d859cc
tuning

diff -r 578460971517 -r a2aa341bc658 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 28 11:43:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 28 11:43:45 2011 +0200
@@ -537,7 +537,7 @@
           Lambda_Lifting.is_quantifier
   #> fst
 
-fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
     intentionalize_def t
   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
     let