src/Pure/logic.ML

   val dest_type: term -> typ
   val const_of_class: class -> string
   val class_of_const: string -> class
   val mk_inclass: typ * class -> term
   val dest_inclass: term -> typ * class
+  val name_classrel: string * string -> string
   val mk_classrel: class * class -> term
   val dest_classrel: term -> class * class
-  val mk_arities: string * sort list * sort -> term list
+  val name_arities: arity -> string list
+  val name_arity: string * sort list * class -> string
+  val mk_arities: arity -> term list
   val dest_arity: term -> string * sort list * class
   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     term -> (term * term) * term
   val abs_def: term -> term * term
   val mk_cond_defpair: term list -> term * term -> string * term

   | dest_inclass t = raise TERM ("dest_inclass", [t]);
 
 
 (* class relations *)
 
+fun name_classrel (c1, c2) =
+  NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
+
 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
 
 fun dest_classrel tm =
   (case dest_inclass tm of
     (TVar (_, [c1]), c2) => (c1, c2)
   | _ => raise TERM ("dest_classrel", [tm]));
 
 
 (* type arities *)
+
+fun name_arities (t, _, S) =
+  let val b = NameSpace.base t
+  in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
+
+fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
   let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
   in map (fn c => mk_inclass (T, c)) S end;