src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

 fun effective_atp_lambda_translation ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>
          if trans = smartN then
            if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+         else if trans = lambdasN andalso
+                 not (is_type_enc_higher_order type_enc) then
+           error ("Lambda translation method incompatible with \
+                  \first-order encoding.")
          else
            trans)
 
 val metis_minimize_max_time = seconds 2.0