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

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 17:29:30 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 17:29:30 2011 +0200
     2.3 @@ -519,6 +519,10 @@
     2.4    |> (fn trans =>
     2.5           if trans = smartN then
     2.6             if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
     2.7 +         else if trans = lambdasN andalso
     2.8 +                 not (is_type_enc_higher_order type_enc) then
     2.9 +           error ("Lambda translation method incompatible with \
    2.10 +                  \first-order encoding.")
    2.11           else
    2.12             trans)
    2.13