suppress irrelevant positions;

--- 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