diff -r fba9754b827e -r 954783662daf src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 17:29:30 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 17:29:30 2011 +0200
@@ -1906,13 +1906,6 @@
         exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_enc) = choose_format [format] type_enc
-    val _ =
-      if lambda_trans = lambdasN andalso
-         not (is_type_enc_higher_order type_enc) then
-        error ("Lambda translation method incompatible with \
-               \first-order encoding.")
-      else
-        ()
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
                          hyp_ts concl_t facts