1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 17:29:30 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 17:29:30 2011 +0200
     1.3 @@ -1906,13 +1906,6 @@
     1.4          exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
     1.5    let
     1.6      val (format, type_enc) = choose_format [format] type_enc
     1.7 -    val _ =
     1.8 -      if lambda_trans = lambdasN andalso
     1.9 -         not (is_type_enc_higher_order type_enc) then
    1.10 -        error ("Lambda translation method incompatible with \
    1.11 -               \first-order encoding.")
    1.12 -      else
    1.13 -        ()
    1.14      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
    1.15        translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
    1.16                           hyp_ts concl_t facts