less bulky "_position", for improved readability of parse trees;

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 22:08:42 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 22:32:49 2011 +0200
@@ -146,7 +146,7 @@
             val c = get_type (Lexicon.str_of_token tok);
             val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
           in [Ast.Constant (Lexicon.mark_type c)] end
-      | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+      | 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))]]

--- a/src/Pure/pure_thy.ML	Tue Apr 19 22:08:42 2011 +0200
+++ b/src/Pure/pure_thy.ML	Tue Apr 19 22:32:49 2011 +0200
@@ -134,8 +134,8 @@
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
     ("_constrainAbs", typ "'a",                        NoSyn),
-    ("_constrain_position", typ "id => id_position",   Delimfix "_"),
-    ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
+    ("_position",   typ "id => id_position",           Delimfix "_"),
+    ("_position",   typ "longid => longid_position",   Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
     ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
     ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),