src/Pure/Syntax/syn_trans.ML

   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
 
 
 (* abstraction *)
 
-fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T;
+fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
 fun mark_bound x = mark_boundT (x, dummyT);
 
 fun bound_vars vars body =
   subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);