diff -r 85c91284ed94 -r 2850b7dc27a4 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 26 14:53:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 26 14:53:00 2011 +0200
@@ -245,6 +245,8 @@
     else
       (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
          (true, [AAbs ((s', ty), tm)]) =>
+         (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
+            possible, to work around LEO-II 1.2.8 parser limitation. *)
          string_for_formula format
              (AQuant (if s = tptp_ho_forall then AForall else AExists,
                       [(s', SOME ty)], AAtom tm))
@@ -256,7 +258,8 @@
              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"
 and string_for_formula format (AQuant (q, xs, phi)) =
     string_for_quantifier q ^