# HG changeset patch
# User blanchet
# Date 1695654992 -7200
# Node ID 1b0f5576f5e9df2a7eeddc3e7484dcf67b97fefd
# Parent  1320782a394eb227a1ef95b940b9748df45f82a5
use same associativity as Isabelle when parsing HOL proofs

diff -r 1320782a394e -r 1b0f5576f5e9 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -541,7 +541,14 @@
 and parse_hol_term x =
   (parse_literal_hol_term -- Scan.repeat (parse_nonliteral_binary_op -- parse_literal_hol_term)
     >> (fn (t1, c_ti_s) =>
-          fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x
+          let
+            val cs = map fst c_ti_s
+            val tis = t1 :: map snd c_ti_s
+            val (tis_but_k, tk) = split_last tis
+          in
+            fold_rev (fn (ti, c) => fn right => mk_apps (mk_simple_aterm c) [ti, right])
+              (tis_but_k ~~ cs) tk
+          end)) x
 
 fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x