# HG changeset patch
# User wenzelm
# Date 1158700539 -7200
# Node ID 2010cbb1a94179fa2621356c117ee687a2e48f93
# Parent  8f6cc81ba4a3e83ac22b6fc47f3d9f1759dd1f92
added name_classrel/arities/arity;

diff -r 8f6cc81ba4a3 -r 2010cbb1a941 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Sep 19 23:15:38 2006 +0200
+++ b/src/Pure/logic.ML	Tue Sep 19 23:15:39 2006 +0200
@@ -35,9 +35,12 @@
   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
@@ -221,6 +224,9 @@
 
 (* 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 =
@@ -231,6 +237,12 @@
 
 (* 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;