avoid duplicate markup, notably from "CONST c";
authorwenzelm
Sun, 15 Dec 2024 21:39:43 +0100
changeset 81599 ca6b2e49424b
parent 81598 82cccc88faa5
child 81600 b1772698bd78
avoid duplicate markup, notably from "CONST c";
src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Dec 15 21:15:18 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Dec 15 21:39:43 2024 +0100
@@ -476,7 +476,7 @@
     fun decode_const ps c = (report ps markup_cache c; Ast.Constant c);
     fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
     fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
-    and decode ps (Ast.Constant c) = decode_const ps c
+    and decode _ (ast as Ast.Constant _) = ast
       | decode ps (Ast.Variable x) =
           if Syntax.is_const syn x orelse Long_Name.is_qualified x
           then decode_const ps x