# HG changeset patch
# User wenzelm
# Date 1320962055 -3600
# Node ID a97251eea45852a0fd008db98398058785544b3d
# Parent  d29d73117b7366911f973bd4c371fe8afff2e1df
suppress irrelevant positions;

diff -r d29d73117b73 -r a97251eea458 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 22:39:32 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 22:54:15 2011 +0100
@@ -155,8 +155,12 @@
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
           if constrain_pos then
-            [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
-              Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
+            let val pos = Lexicon.pos_of_token tok in
+              if Position.is_reported pos then
+                [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+                  Ast.Variable (Term_Position.encode pos)]]
+              else [ast_of pt]
+            end
           else [ast_of pt]
       | asts_of (Parser.Node (a, pts)) =
           let