naming policy for instances
authorhaftmann
Wed, 28 Nov 2007 09:01:50 +0100
changeset 25486 b944ef973109
parent 25485 33840a854e63
child 25487 d96d5808d926
naming policy for instances
src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Nov 28 09:01:42 2007 +0100
+++ b/src/Pure/axclass.ML	Wed Nov 28 09:01:50 2007 +0100
@@ -26,6 +26,7 @@
   val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
   val axiomatize_arity: arity -> theory -> theory
   val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
+  val instance_name: string * class -> string
   type cache
   val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
   val cache: cache
@@ -132,6 +133,8 @@
 
 (* maintain instances *)
 
+fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
+
 val get_instances = #2 o AxClassData.get;
 fun map_instances f = AxClassData.map (apsnd f);