1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 11:21:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -1258,7 +1258,8 @@
     1.4      fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
     1.5        | aux arity (IConst (name as (s, _), T, T_args)) =
     1.6          (case strip_prefix_and_unascii const_prefix s of
     1.7 -           NONE => (name, T_args)
     1.8 +           NONE =>
     1.9 +           (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
    1.10           | SOME s'' =>
    1.11             let
    1.12               val s'' = invert_const s''

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 11:21:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 14:10:12 2011 +0200
     2.3 @@ -525,10 +525,14 @@
     2.4     | NONE => type_enc_from_string best_type_enc)
     2.5    |> choose_format formats
     2.6  
     2.7 -fun lift_lambdas ctxt =
     2.8 +fun lift_lambdas ctxt type_enc =
     2.9    map (close_form o Envir.eta_contract) #> rpair ctxt
    2.10 -  #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
    2.11 -                                  Lambda_Lifting.is_quantifier
    2.12 +  #-> Lambda_Lifting.lift_lambdas
    2.13 +          (if polymorphism_of_type_enc type_enc = Polymorphic then
    2.14 +             SOME polymorphic_free_prefix
    2.15 +           else
    2.16 +             NONE)
    2.17 +          Lambda_Lifting.is_quantifier
    2.18    #> fst
    2.19  
    2.20  fun translate_atp_lambdas ctxt type_enc =
    2.21 @@ -544,9 +548,9 @@
    2.22             trans)
    2.23    |> (fn trans =>
    2.24           if trans = concealedN then
    2.25 -           lift_lambdas ctxt ##> K []
    2.26 +           lift_lambdas ctxt type_enc ##> K []
    2.27           else if trans = liftingN then
    2.28 -           lift_lambdas ctxt
    2.29 +           lift_lambdas ctxt type_enc
    2.30           else if trans = combinatorsN then
    2.31             map (introduce_combinators ctxt) #> rpair []
    2.32           else if trans = lambdasN then