1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4            s ^ "(" ^ commas ss ^ ")"
     1.5        end
     1.6    | string_for_term THF (AAbs ((s, ty), tm)) =
     1.7 -    "^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm
     1.8 +    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
     1.9    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.10  
    1.11  fun string_for_quantifier AForall = tptp_forall