--- 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