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 @@ -218,25 +218,6 @@
     1.4         tptp_fun_type ^ " " ^ s)
     1.5    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
     1.6  
     1.7 -fun string_for_term _ (ATerm (s, [])) = s
     1.8 -  | string_for_term format (ATerm (s, ts)) =
     1.9 -    if s = tptp_empty_list then
    1.10 -      (* used for lists in the optional "source" field of a derivation *)
    1.11 -      "[" ^ commas (map (string_for_term format) ts) ^ "]"
    1.12 -    else if is_tptp_equal s then
    1.13 -      space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
    1.14 -      |> format = THF ? enclose "(" ")"
    1.15 -    else
    1.16 -      let val ss = map (string_for_term format) ts in
    1.17 -        if format = THF then
    1.18 -          "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
    1.19 -        else
    1.20 -          s ^ "(" ^ commas ss ^ ")"
    1.21 -      end
    1.22 -  | string_for_term THF (AAbs ((s, ty), tm)) =
    1.23 -    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
    1.24 -  | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.25 -
    1.26  fun string_for_quantifier AForall = tptp_forall
    1.27    | string_for_quantifier AExists = tptp_exists
    1.28  
    1.29 @@ -253,7 +234,31 @@
    1.30         else
    1.31           "")
    1.32  
    1.33 -fun string_for_formula format (AQuant (q, xs, phi)) =
    1.34 +fun string_for_term _ (ATerm (s, [])) = s
    1.35 +  | string_for_term format (ATerm (s, ts)) =
    1.36 +    if s = tptp_empty_list then
    1.37 +      (* used for lists in the optional "source" field of a derivation *)
    1.38 +      "[" ^ commas (map (string_for_term format) ts) ^ "]"
    1.39 +    else if is_tptp_equal s then
    1.40 +      space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
    1.41 +      |> format = THF ? enclose "(" ")"
    1.42 +    else
    1.43 +      (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
    1.44 +         (true, [AAbs ((s', ty), tm)]) =>
    1.45 +         string_for_formula format
    1.46 +             (AQuant (if s = tptp_ho_forall then AForall else AExists,
    1.47 +                      [(s', SOME ty)], AAtom tm))
    1.48 +       | _ =>
    1.49 +         let val ss = map (string_for_term format) ts in
    1.50 +           if format = THF then
    1.51 +             "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
    1.52 +           else
    1.53 +             s ^ "(" ^ commas ss ^ ")"
    1.54 +         end)
    1.55 +  | string_for_term THF (AAbs ((s, ty), tm)) =
    1.56 +    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
    1.57 +  | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.58 +and string_for_formula format (AQuant (q, xs, phi)) =
    1.59      string_for_quantifier q ^
    1.60      "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
    1.61      string_for_formula format phi