src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

   (case type_enc_opt of
      SOME ts => ts
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
-fun lift_lambdas ctxt =
+fun lift_lambdas ctxt type_enc =
   map (close_form o Envir.eta_contract) #> rpair ctxt
-  #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
-                                  Lambda_Lifting.is_quantifier
+  #-> Lambda_Lifting.lift_lambdas
+          (if polymorphism_of_type_enc type_enc = Polymorphic then
+             SOME polymorphic_free_prefix
+           else
+             NONE)
+          Lambda_Lifting.is_quantifier
   #> fst
 
 fun translate_atp_lambdas ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>

                   \encoding.")
          else
            trans)
   |> (fn trans =>
          if trans = concealedN then
-           lift_lambdas ctxt ##> K []
+           lift_lambdas ctxt type_enc ##> K []
          else if trans = liftingN then
-           lift_lambdas ctxt
+           lift_lambdas ctxt type_enc
          else if trans = combinatorsN then
            map (introduce_combinators ctxt) #> rpair []
          else if trans = lambdasN then
            map (Envir.eta_contract) #> rpair []
          else