# HG changeset patch
# User fleury
# Date 1410521252 -7200
# Node ID 65651cb9d191064fb10e098e273d730e7a420c6d
# Parent  29b8688c5f76154667a8ea0183355c472d9421f6
correction in the thf0 parser ("(=)" found in a Satallax proof).

diff -r 29b8688c5f76 -r 65651cb9d191 src/HOL/Tools/ATP/atp_proof.ML
--- 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