diff -r d56a9267eb1a -r 611f4ef94901 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 10 15:48:07 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 10 16:26:54 2020 +0100
@@ -99,7 +99,7 @@
   val is_type_enc_sound : type_enc -> bool
   val type_enc_of_string : strictness -> string -> type_enc
   val adjust_type_enc : atp_format -> type_enc -> type_enc
-  val is_lambda_free : term -> bool
+  val is_first_order_lambda_free : term -> bool
   val do_cheaply_conceal_lambdas : typ list -> term -> term
   val mk_aconns :
     atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
@@ -728,42 +728,62 @@
     (if is_type_enc_sound type_enc then Tags else Guards) stuff
   | adjust_type_enc _ type_enc = type_enc
 
-fun is_lambda_free t =
+fun is_first_order_lambda_free t =
   (case t of
-    \<^const>\<open>Not\<close> $ t1 => is_lambda_free t1
-  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
-  | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_lambda_free t1
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_lambda_free t1
-  | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
-  | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
-  | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
+    \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
+  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+  | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
+  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+  | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
+  | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
+    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
-    is_lambda_free t1 andalso is_lambda_free t2
+    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
 
-fun simple_translate_lambdas do_lambdas ctxt t =
-  if is_lambda_free t then
+fun simple_translate_lambdas do_lambdas ctxt type_enc t =
+  if is_first_order_lambda_free t then
     t
   else
     let
-      fun trans Ts t =
+      fun trans_first_order Ts t =
         (case t of
-          \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans Ts t1
+          \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
         | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
-          t0 $ Abs (s, T, trans (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
+          t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+          trans_first_order Ts (t0 $ eta_expand Ts t1 1)
         | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
-          t0 $ Abs (s, T, trans (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
-        | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
-        | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
-        | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
+          t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+          trans_first_order Ts (t0 $ eta_expand Ts t1 1)
+        | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+        | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+        | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
         | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
-          t0 $ trans Ts t1 $ trans Ts t2
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
         | _ =>
           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
           else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
+
+      fun trans_fool Ts t =
+        (case t of
+          (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+          t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+          t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+        | t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2
+        | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts
+        | _ => t)
+
+      val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order
       val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
     in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
 
@@ -809,18 +829,18 @@
           Lambda_Lifting.is_quantifier
   #> fst
 
-fun lift_lams_part_2 ctxt (facts, lifted) =
+fun lift_lams_part_2 ctxt type_enc (facts, lifted) =
   (facts, lifted)
   (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
      get rid of them *)
-  |> apply2 (map (introduce_combinators ctxt))
+  |> apply2 (map (introduce_combinators ctxt type_enc))
   |> apply2 (map constify_lifted)
   (* Requires bound variables not to clash with any schematic variables (as
      should be the case right after lambda-lifting). *)
   |>> map (hol_open_form (unprefix hol_close_form_prefix))
   ||> map (hol_open_form I)
 
-fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
+fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc
 
 fun intentionalize_def (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) =
     intentionalize_def t
@@ -1887,17 +1907,17 @@
   else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
     lift_lams ctxt type_enc
   else if lam_trans = combsN then
-    map (introduce_combinators ctxt) #> rpair []
+    map (introduce_combinators ctxt type_enc) #> rpair []
   else if lam_trans = combs_and_liftingN then
     lift_lams_part_1 ctxt type_enc
-    ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
-    #> lift_lams_part_2 ctxt
+    ##> maps (fn t => [t, introduce_combinators ctxt type_enc (intentionalize_def t)])
+    #> lift_lams_part_2 ctxt type_enc
   else if lam_trans = combs_or_liftingN then
     lift_lams_part_1 ctxt type_enc
     ##> map (fn t => (case head_of (strip_qnt_body \<^const_name>\<open>All\<close> t) of
                        \<^term>\<open>(=) ::bool => bool => bool\<close> => t
-                     | _ => introduce_combinators ctxt (intentionalize_def t)))
-    #> lift_lams_part_2 ctxt
+                     | _ => introduce_combinators ctxt type_enc (intentionalize_def t)))
+    #> lift_lams_part_2 ctxt type_enc
   else if lam_trans = keep_lamsN then
     map (Envir.eta_contract) #> rpair []
   else