no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);
authorwenzelm
Fri, 20 Sep 2024 11:10:04 +0200
changeset 80907 5703399d9c56
parent 80906 fb03de505aee
child 80908 d794caea94a5
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);
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;