src/Pure/Syntax/syntax_phases.ML

 
     fun ast_of_position tok =
       Ast.Variable (Term_Position.encode (report_pos tok));
 
     fun ast_of_dummy a tok =
-      Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
+      Ast.constrain (Ast.Constant a) (ast_of_position tok);
 
     fun asts_of_position c tok =
       [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
     and asts_of (Parser.Markup ({markup, range = (pos, _), ...}, pts)) =

     val clean_var_types = show_markup andalso not show_types;
 
     fun constrain clean T ast =
       let val U = Type_Annotation.print clean T in
         if U = dummyT then ast
-        else Ast.Appl [Ast.Constant "_constrain", ast, ast_of_termT ctxt trf (term_of_typ ctxt U)]
+        else Ast.constrain ast (ast_of_termT ctxt trf (term_of_typ ctxt U))
       end;
 
     fun main tm =
       (case strip_comb tm of
         (t as Abs _, ts) => Ast.mk_appl (main (Syntax_Trans.abs_tr' ctxt t)) (map main ts)

     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
         val pos = the_default Position.none (Term_Position.decode p);
         val (c', _) = decode_const ctxt (c, [pos]);
         val d = if intern then Lexicon.mark_const c' else c;
-      in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
+      in Ast.constrain (Ast.Constant d) T end
   | _ => raise Ast.AST ("const_ast_tr", asts));
 
 
 (* setup translations *)