# HG changeset patch
# User wenzelm
# Date 1726823963 -7200
# Node ID d794caea94a547716c077441fe56d1fdce09f7b9
# Parent  5703399d9c5674bec836f7eeb2f35c164cb3a7bf
tuned;

diff -r 5703399d9c56 -r d794caea94a5 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 11:10:04 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 11:19:23 2024 +0200
@@ -284,9 +284,10 @@
     val _ = Context_Position.reports_text ctxt (maps reports_text_of xsymbs);
   in xsymbs end;
 
-fun mfix_args ctxt =
-  let val ctxt' = Context_Position.set_visible false ctxt
-  in length o filter (is_argument o #1) o read_mfix ctxt' end;
+val read_mfix0 = read_mfix o Context_Position.set_visible false;
+
+fun mfix_args ctxt ss =
+  Integer.build (read_mfix0 ctxt ss |> fold (fn (xsymb, _) => is_argument xsymb ? Integer.add 1));
 
 fun mixfix_args ctxt = mfix_args ctxt o Input.source_explode;