author blanchet Tue, 10 Jul 2012 23:36:03 +0200 changeset 48231 8fa803f5a731 parent 48230 0feb93dfb268 child 48232 712d49104b13
tuning
--- 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