# HG changeset patch
# User blanchet
# Date 1643716113 -3600
# Node ID 9e1d486e2d9f608d4350fb719815425fa8da218f
# Parent  1a8f6cb5efd602477b02b29a5e3808a697b4eb4e
careful with partial applications

diff -r 1a8f6cb5efd6 -r 9e1d486e2d9f src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 01 12:32:33 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 01 12:48:33 2022 +0100
@@ -275,7 +275,7 @@
         else if s = tptp_equal then
           list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
             map (do_term NONE) us)
-        else if s = tptp_not_equal then
+        else if s = tptp_not_equal andalso length us = 2 then
           \<^const>\<open>HOL.Not\<close> $ list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
             map (do_term NONE) us)
         else if not (null us) then
@@ -288,7 +288,7 @@
         else if s = tptp_and then HOLogic.conj
         else if s = tptp_implies then HOLogic.imp
         else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT
-        else if s = tptp_not_iff then \<^term>\<open>\<lambda>x y. x \<noteq> y\<close>
+        else if s = tptp_not_iff orelse s = tptp_not_equal then \<^term>\<open>\<lambda>x y. x \<noteq> y\<close>
         else if s = tptp_if then \<^term>\<open>\<lambda>P Q. Q \<longrightarrow> P\<close>
         else if s = tptp_not_and then \<^term>\<open>\<lambda>P Q. \<not> (P \<and> Q)\<close>
         else if s = tptp_not_or then \<^term>\<open>\<lambda>P Q. \<not> (P \<or> Q)\<close>