# HG changeset patch
# User blanchet
# Date 1626100217 -7200
# Node ID b304285fd80012dd799366207314d40c532aa42b
# Parent  96a05b8462f952029c8654044388dcd334d048f6
parse logical operators in the right order w.r.t. backtracking

diff -r 96a05b8462f9 -r b304285fd800 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:16 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:17 2021 +0200
@@ -476,8 +476,8 @@
   | role_of_tptp_string _ = Unknown
 
 val tptp_binary_ops =
-  [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
-   tptp_equal, tptp_not_equal, tptp_app]
+  [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and,
+   tptp_not_or, tptp_not_iff, tptp_app]
 
 fun parse_one_in_list xs =
   foldl1 (op ||) (map Scan.this_string xs)