diff -r 38ac2e714729 -r 8ce08b154aa1 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jul 20 11:48:30 2019 +0200
+++ b/src/Pure/logic.ML	Sat Jul 20 12:52:29 2019 +0200
@@ -54,6 +54,7 @@
   val name_arities: arity -> string list
   val name_arity: string * sort list * class -> string
   val mk_arities: arity -> term list
+  val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
   val unconstrainT: sort list -> term ->
     ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
@@ -319,6 +320,8 @@
   let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
   in map (fn c => mk_of_class (T, c)) S end;
 
+fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
+
 fun dest_arity tm =
   let
     fun err () = raise TERM ("dest_arity", [tm]);