merged

--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 17:15:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 19:43:45 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

--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 17:15:24 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 19:43:45 2011 +0200
@@ -38,7 +38,7 @@
   (*translation*)
   val add_config: SMT_Utils.class * (Proof.context -> config) ->
     Context.generic -> Context.generic 
-  val lift_lambdas: Proof.context -> term list ->
+  val lift_lambdas: Proof.context -> bool -> term list ->
     Proof.context * (term list * term list)
   val translate: Proof.context -> string list -> (int * thm) list ->
     string * recon
@@ -246,22 +246,25 @@
 (** lambda-lifting **)
 
 local
-  fun mk_def Ts T lhs rhs =
+  fun mk_def triggers Ts T lhs rhs =
     let
       val eq = HOLogic.eq_const T $ lhs $ rhs
-      val trigger =
+      fun trigger () =
         [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
         |> map (HOLogic.mk_list @{typ SMT.pattern})
         |> HOLogic.mk_list @{typ "SMT.pattern list"}
       fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
-    in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end
+    in
+      fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq
+        else eq)
+    end
 
   fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts
 
   fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
     | dest_abs Ts t = (Ts, t)
 
-  fun replace_lambda Us Ts t (cx as (defs, ctxt)) =
+  fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
     let
       val t1 = mk_abs Us t
       val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
@@ -284,31 +287,32 @@
             val (is, UTs) = split_list (map_index I (Us @ Ts'))
             val f = Free (n, rev UTs ---> T)
             val lhs = Term.list_comb (f, map Bound (rev is))
-            val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
+            val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
           in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
     end
 
-  fun traverse Ts t =
+  fun traverse triggers Ts t =
     (case t of
       (q as Const (@{const_name All}, _)) $ Abs a =>
-        abs_traverse Ts a #>> (fn a' => q $ Abs a')
+        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
     | (q as Const (@{const_name Ex}, _)) $ Abs a =>
-        abs_traverse Ts a #>> (fn a' => q $ Abs a')
+        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
     | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
-        traverse Ts u ##>> abs_traverse Ts a #>>
+        traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
         (fn (u', a') => l $ u' $ Abs a')
     | Abs _ =>
         let val (Us, u) = dest_abs [] t
-        in traverse (Us @ Ts) u #-> replace_lambda Us Ts end
-    | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $)
+        in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
+    | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
     | _ => pair t)
 
-  and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t'))
+  and abs_traverse triggers Ts (n, T, t) =
+    traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
 in
 
-fun lift_lambdas ctxt ts =
+fun lift_lambdas ctxt triggers ts =
   (Termtab.empty, ctxt)
-  |> fold_map (traverse []) ts
+  |> fold_map (traverse triggers []) ts
   |> (fn (us, (defs, ctxt')) =>
        (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
 
@@ -614,7 +618,7 @@
     val (ctxt2, ts3) =
       ts2
       |> eta_expand ctxt1 is_fol funcs
-      |> lift_lambdas ctxt1
+      |> lift_lambdas ctxt1 true
       ||> (op @)
       |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 17:15:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 19:43:45 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)