# HG changeset patch
# User wenzelm
# Date 1733861164 -3600
# Node ID 693a95492008c77ad706de61efcfc39389298b51
# Parent  a180b070d4f8d6077f14a9ef9b00981843da7b74
more accurate markup for "CONST c";

diff -r a180b070d4f8 -r 693a95492008 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Dec 10 19:47:47 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Dec 10 21:06:04 2024 +0100
@@ -877,8 +877,8 @@
   (case asts of
     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
-        val (c', _) = decode_const ctxt (c, map #pos (Term_Position.decode p));
-        val d = if intern then Lexicon.mark_const c' else c;
+        val (c', reports) = decode_const ctxt (c, map #pos (Term_Position.decode p));
+        val d = if intern then (Context_Position.reports ctxt reports; Lexicon.mark_const c') else c;
       in Ast.constrain (Ast.Constant d) T end
   | _ => raise Ast.AST ("const_ast_tr", asts));