# HG changeset patch
# User blanchet
# Date 1318945258 -7200
# Node ID 6bc8d260d459296e7735d95c5e45a6e8dcf175c6
# Parent  861ab6f9eb2b4352873f291e6faa5b3e60e3dc3a
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations

diff -r 861ab6f9eb2b -r 6bc8d260d459 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Oct 18 15:27:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Oct 18 15:40:58 2011 +0200
@@ -946,10 +946,8 @@
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)
-          | NONE => if s = tptp_choice then
-                      tweak_ho_quant tptp_choice T args
-                    else
-                      IConst (name, T, T_args))
+          | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
+                    else IConst (name, T, T_args))
       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
       | intro _ _ tm = tm
   in intro true [] end
@@ -1049,8 +1047,12 @@
       | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
         do_quant bs AForall pos s T t'
+      | (t0 as Const (@{const_name All}, _)) $ t1 =>
+        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
         do_quant bs AExists pos s T t'
+      | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
       | @{const HOL.implies} $ t1 $ t2 =>