correction in the thf0 parser ("(=)" found in a Satallax proof).

--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Sep 12 11:17:06 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Sep 12 13:27:32 2014 +0200
@@ -533,7 +533,8 @@
   || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
   || parse_ho_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_thf0_term --| $$ ")"
-  || scan_general_id >> mk_simple_aterm) x
+  || scan_general_id >> mk_simple_aterm
+  || parse_binary_op >> mk_simple_aterm) x
 and parse_thf0_term x =
   (parse_simple_thf0_term
       -- Scan.option (parse_binary_op