src/HOL/Tools/ATP/atp_problem.ML

           "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
         else
           s ^ "(" ^ commas ss ^ ")"
       end
   | string_for_term THF (AAbs ((s, ty), tm)) =
-    "^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm
+    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
   | string_for_term _ _ = raise Fail "unexpected term in first-order format"
 
 fun string_for_quantifier AForall = tptp_forall
   | string_for_quantifier AExists = tptp_exists