diff -r 71756d95b7df -r 51c338103975 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Tue Sep 17 18:49:46 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Thu Sep 19 12:08:56 2024 +0200 @@ -291,7 +291,7 @@ val nonterm_for_lhs = the_default "logic" o try dest_Type_name; val nonterm_for_rhs = the_default "any" o try dest_Type_name; - val _ = Position.report pos Markup.language_mixfix; + val _ = Context_Position.report ctxt pos Markup.language_mixfix; val symbs0 = read_mfix ctxt sy; fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);