# HG changeset patch
# User wenzelm
# Date 1726823404 -7200
# Node ID 5703399d9c5674bec836f7eeb2f35c164cb3a7bf
# Parent  fb03de505aee7916b14f879d8aad0e5a9fff193e
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);

diff -r fb03de505aee -r 5703399d9c56 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 11:04:35 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 11:10:04 2024 +0200
@@ -286,7 +286,7 @@
 
 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' o map (apsnd (K Position.none)) end;
+  in length o filter (is_argument o #1) o read_mfix ctxt' end;
 
 fun mixfix_args ctxt = mfix_args ctxt o Input.source_explode;