# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 8fa803f5a7319a2de707f339ba5d7ea320faa4da
# Parent  0feb93dfb268230da5d6f5314d511cf18c37dd33
tuning

diff -r 0feb93dfb268 -r 8fa803f5a731 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -94,6 +94,7 @@
   val is_type_enc_sound : type_enc -> bool
   val type_enc_from_string : strictness -> string -> type_enc
   val adjust_type_enc : atp_format -> type_enc -> type_enc
+  val has_no_lambdas : term -> bool
   val mk_aconns :
     connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -702,22 +703,22 @@
     (if is_type_enc_sound type_enc then Tags else Guards) stuff
   | adjust_type_enc _ type_enc = type_enc
 
-fun is_fol_term t =
+fun has_no_lambdas t =
   case t of
-    @{const Not} $ t1 => is_fol_term t1
-  | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'
-  | Const (@{const_name All}, _) $ t1 => is_fol_term t1
-  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'
-  | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1
-  | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
-  | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
-  | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
+    @{const Not} $ t1 => has_no_lambdas t1
+  | Const (@{const_name All}, _) $ Abs (_, _, t') => has_no_lambdas t'
+  | Const (@{const_name All}, _) $ t1 => has_no_lambdas t1
+  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => has_no_lambdas t'
+  | Const (@{const_name Ex}, _) $ t1 => has_no_lambdas t1
+  | @{const HOL.conj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
+  | @{const HOL.disj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
+  | @{const HOL.implies} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
   | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
-    is_fol_term t1 andalso is_fol_term t2
+    has_no_lambdas t1 andalso has_no_lambdas t2
   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
 
 fun simple_translate_lambdas do_lambdas ctxt t =
-  if is_fol_term t then
+  if has_no_lambdas t then
     t
   else
     let