src/Pure/Syntax/syntax_ext.ML
changeset 80899 51c338103975
parent 80897 5328d67ec647
child 80904 05f17df447b6
--- 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);