# HG changeset patch
# User blanchet
# Date 1643712701 -3600
# Node ID e926618f94745d59e608a0ffff8cc7758994d71b
# Parent  7d2a5d1f09af8619595066e4fe1d538f70cef58c
handle TPTP '!=' more gracefully in Isar proof reconstruction

diff -r 7d2a5d1f09af -r e926618f9474 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 01 10:58:09 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 01 11:51:41 2022 +0100
@@ -275,6 +275,9 @@
         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
+          \<^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
           let
             val args = map (do_term NONE) us
@@ -285,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 orelse s = tptp_not_equal then \<^term>\<open>\<lambda>P Q. Q \<noteq> P\<close>
+        else if s = tptp_not_iff 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>
@@ -568,7 +571,6 @@
 fun infer_formulas_types ctxt =
   map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT))
   #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-  #> map (set_var_index 0)
 
 val combinator_table =
   [(\<^const_name>\<open>Meson.COMBI\<close>, @{thm Meson.COMBI_def [abs_def]}),