# HG changeset patch
# User wenzelm
# Date 1303245169 -7200
# Node ID 16bc5564535f62c37fa3c7d633afb3a7ad5dc8d2
# Parent  3e1e80df6a4259f302f18bc47e5d166116923b52
less bulky "_position", for improved readability of parse trees;

diff -r 3e1e80df6a42 -r 16bc5564535f src/Pure/Syntax/syntax_phases.ML
--- 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))]]
diff -r 3e1e80df6a42 -r 16bc5564535f src/Pure/pure_thy.ML
--- 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 _"),