# HG changeset patch
# User blanchet
# Date 1695654992 -7200
# Node ID 1320782a394eb227a1ef95b940b9748df45f82a5
# Parent  e10ef4f9c84847ac381ee7fe6775257bbd27b69a
improved Sledgehammer's HOL proof parser w.r.t. negation

diff -r e10ef4f9c848 -r 1320782a394e src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -524,7 +524,7 @@
                     else
                       I))
             ys t)
-  || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not)
+  || Scan.this_string tptp_not |-- parse_simple_hol_term >> mk_app (mk_simple_aterm tptp_not)
   || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
     >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
   || parse_hol_quantifier >> mk_simple_aterm