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