# HG changeset patch
# User blanchet
# Date 1310657370 -7200
# Node ID 954783662daf1c9b239d3989831ae08a77520be7
# Parent  fba9754b827e5050fefb25fe0e7b5ae686767b26
move error logic closer to user

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
diff -r fba9754b827e -r 954783662daf src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 17:29:30 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 17:29:30 2011 +0200
@@ -519,6 +519,10 @@
   |> (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)