position constraint for bound dummy -- more PIDE markup;

--- a/src/Pure/Syntax/syntax_phases.ML	Sun May 26 21:53:10 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun May 26 22:47:00 2013 +0200
@@ -154,6 +154,10 @@
     fun ast_of_position tok =
       Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
 
+    fun ast_of_dummy a tok =
+      if raw then Ast.Constant a
+      else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
+
     fun asts_of_position c tok =
       if raw then asts_of_token tok
       else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
@@ -176,8 +180,11 @@
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
       | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
-          if raw then [Ast.Constant a]
-          else [Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]]
+          [ast_of_dummy a tok]
+      | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
+          [ast_of_dummy a tok]
+      | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
+          [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
       | asts_of (Parser.Node (a, pts)) =
           let
             val _ = pts |> List.app

--- a/src/Pure/Syntax/syntax_trans.ML	Sun May 26 21:53:10 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Sun May 26 22:47:00 2013 +0200
@@ -121,9 +121,6 @@
 fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
   | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
 
-fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
-  | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
 fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
 
@@ -513,7 +510,6 @@
   ("_applC", fn _ => applC_ast_tr),
   ("_lambda", fn _ => lambda_ast_tr),
   ("_idtyp", fn _ => idtyp_ast_tr),
-  ("_idtypdummy", fn _ => idtypdummy_ast_tr),
   ("_bigimpl", fn _ => bigimpl_ast_tr),
   ("_indexdefault", fn _ => indexdefault_ast_tr),
   ("_indexvar", fn _ => indexvar_ast_tr),