1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 28 11:43:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 28 11:43:45 2011 +0200
     1.3 @@ -537,7 +537,7 @@
     1.4            Lambda_Lifting.is_quantifier
     1.5    #> fst
     1.6  
     1.7 -fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) =
     1.8 +fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
     1.9      intentionalize_def t
    1.10    | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    1.11      let