# 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