# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 4d4f2721b3ef22a758aea6dfd5b1faa113ca3c89
# Parent  446cfc760ccf39471ffd166b0b55b989ebe6eadc
fixed eta-extension of higher-order quantifiers in THF output

diff -r 446cfc760ccf -r 4d4f2721b3ef src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -1909,8 +1909,18 @@
   |> ho_term_from_iterm ctxt format mono type_enc pos
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt format mono type_enc =
+and ho_term_from_iterm ctxt format mono type_enc pos =
   let
+    fun beta_red bs (IApp (IAbs ((name, _), tm), tm')) =
+        beta_red ((name, beta_red bs tm') :: bs) tm
+      | beta_red bs (IApp tmp) = IApp (pairself (beta_red bs) tmp)
+      | beta_red bs (tm as IConst (name, _, _)) =
+        (case AList.lookup (op =) bs name of
+           SOME tm' => tm'
+         | NONE => tm)
+      | beta_red bs (IAbs ((name, T), tm)) =
+        IAbs ((name, T), beta_red (AList.delete (op =) name bs) tm)
+      | beta_red _ tm = tm
     fun term site u =
       let
         val (head, args) = strip_iterm_comb u
@@ -1922,7 +1932,9 @@
         val t =
           case head of
             IConst (name as (s, _), _, T_args) =>
-            let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in
+            let
+              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
+            in
               map (term arg_site) args |> mk_aterm format type_enc name T_args
             end
           | IVar (name, _) =>
@@ -1941,7 +1953,7 @@
         else
           t
       end
-  in term o Top_Level end
+  in term (Top_Level pos) o beta_red [] end
 and formula_from_iformula ctxt polym_constrs format mono type_enc
                           should_guard_var =
   let