--- 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]);