1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 26 14:53:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 26 14:53:00 2011 +0200
     1.3 @@ -245,6 +245,8 @@
     1.4      else
     1.5        (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
     1.6           (true, [AAbs ((s', ty), tm)]) =>
     1.7 +         (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
     1.8 +            possible, to work around LEO-II 1.2.8 parser limitation. *)
     1.9           string_for_formula format
    1.10               (AQuant (if s = tptp_ho_forall then AForall else AExists,
    1.11                        [(s', SOME ty)], AAtom tm))
    1.12 @@ -256,7 +258,8 @@
    1.13               s ^ "(" ^ commas ss ^ ")"
    1.14           end)
    1.15    | string_for_term THF (AAbs ((s, ty), tm)) =
    1.16 -    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
    1.17 +    "(^[" ^ s ^ " : " ^ string_for_type THF ty ^ "] : " ^
    1.18 +    string_for_term THF tm ^ ")"
    1.19    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.20  and string_for_formula format (AQuant (q, xs, phi)) =
    1.21      string_for_quantifier q ^

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     2.3 @@ -805,32 +805,44 @@
     2.4  
     2.5  fun introduce_proxies type_enc =
     2.6    let
     2.7 -    fun intro top_level (IApp (tm1, tm2)) =
     2.8 -        IApp (intro top_level tm1, intro false tm2)
     2.9 -      | intro top_level (IConst (name as (s, _), T, T_args)) =
    2.10 +    fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
    2.11 +      | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
    2.12 +                       _ =
    2.13 +        (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
    2.14 +           limitation. This works in conjuction with special code in
    2.15 +           "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
    2.16 +           possible. *)
    2.17 +        IAbs ((`I "P", p_T),
    2.18 +              IApp (IConst (`I ho_quant, T, []),
    2.19 +                    IAbs ((`I "X", x_T),
    2.20 +                          IApp (IConst (`I "P", p_T, []),
    2.21 +                                IConst (`I "X", x_T, [])))))
    2.22 +      | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
    2.23 +    fun intro top_level args (IApp (tm1, tm2)) =
    2.24 +        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
    2.25 +      | intro top_level args (IConst (name as (s, _), T, T_args)) =
    2.26          (case proxify_const s of
    2.27             SOME proxy_base =>
    2.28             if top_level orelse is_type_enc_higher_order type_enc then
    2.29               case (top_level, s) of
    2.30 -               (_, "c_False") => (`I tptp_false, [])
    2.31 -             | (_, "c_True") => (`I tptp_true, [])
    2.32 -             | (false, "c_Not") => (`I tptp_not, [])
    2.33 -             | (false, "c_conj") => (`I tptp_and, [])
    2.34 -             | (false, "c_disj") => (`I tptp_or, [])
    2.35 -             | (false, "c_implies") => (`I tptp_implies, [])
    2.36 -             | (false, "c_All") => (`I tptp_ho_forall, [])
    2.37 -             | (false, "c_Ex") => (`I tptp_ho_exists, [])
    2.38 +               (_, "c_False") => IConst (`I tptp_false, T, [])
    2.39 +             | (_, "c_True") => IConst (`I tptp_true, T, [])
    2.40 +             | (false, "c_Not") => IConst (`I tptp_not, T, [])
    2.41 +             | (false, "c_conj") => IConst (`I tptp_and, T, [])
    2.42 +             | (false, "c_disj") => IConst (`I tptp_or, T, [])
    2.43 +             | (false, "c_implies") => IConst (`I tptp_implies, T, [])
    2.44 +             | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
    2.45 +             | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
    2.46               | (false, s) =>
    2.47 -               if is_tptp_equal s then (`I tptp_equal, [])
    2.48 -               else (proxy_base |>> prefix const_prefix, T_args)
    2.49 -             | _ => (name, [])
    2.50 +               if is_tptp_equal s then IConst (`I tptp_equal, T, [])
    2.51 +               else IConst (proxy_base |>> prefix const_prefix, T, T_args)
    2.52 +             | _ => IConst (name, T, [])
    2.53             else
    2.54 -             (proxy_base |>> prefix const_prefix, T_args)
    2.55 -          | NONE => (name, T_args))
    2.56 -        |> (fn (name, T_args) => IConst (name, T, T_args))
    2.57 -      | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm)
    2.58 -      | intro _ tm = tm
    2.59 -  in intro true end
    2.60 +             IConst (proxy_base |>> prefix const_prefix, T, T_args)
    2.61 +          | NONE => IConst (name, T, T_args))
    2.62 +      | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
    2.63 +      | intro _ _ tm = tm
    2.64 +  in intro true [] end
    2.65  
    2.66  fun iformula_from_prop thy type_enc eq_as_iff =
    2.67    let