# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 4cdefee3f97f59b4c3b5b9935d28fa0ffbdddbaa
# Parent  4a6eb1b1834060f84e8e721beeba56e996f0f1e4
more robust E proof parsing

diff -r 4a6eb1b18340 -r 4cdefee3f97f src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -64,6 +64,7 @@
 
   val tptp_cnf : string
   val tptp_fof : string
+  val tptp_tcf : string
   val tptp_tff : string
   val tptp_thf : string
   val tptp_has_type : string
@@ -222,6 +223,7 @@
 (* official TPTP syntax *)
 val tptp_cnf = "cnf"
 val tptp_fof = "fof"
+val tptp_tcf = "tcf" (* sometimes appears in E's output *)
 val tptp_tff = "tff"
 val tptp_thf = "thf"
 val tptp_has_type = ":"
diff -r 4a6eb1b18340 -r 4cdefee3f97f src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -572,7 +572,8 @@
       end)
 
 fun parse_tstp_fol_line full problem =
-  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
+  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tcf
+      || Scan.this_string tptp_tff) -- $$ "(")
     |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
     -- (if full then parse_fol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
     -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."