src/Pure/Syntax/syn_trans.ML

 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
       Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
   | type_tr' _ _ _ = raise Match;
 
 
+(* type constraints *)
+
+fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
+      Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
+  | type_constraint_tr' _ _ _ = raise Match;
+
+
 (* dependent / nondependent quantifiers *)
 
 fun variant_abs' (x, T, B) =
   let val x' = variant (add_term_names (B, [])) x in
     (x', subst_bound (mark_boundT (x', T), B))

   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
    ("_index", index_ast_tr')]);
 
 val pure_trfunsT =
-  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
+  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr'),
+   ("_type_constraint_", type_constraint_tr')];
 
 fun struct_trfuns structs =
   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);