# HG changeset patch
# User haftmann
# Date 1196236910 -3600
# Node ID b944ef973109a08f89eff30a760fc58fbb1137d8
# Parent  33840a854e6328eab93866946ed1d3837c99d115
naming policy for instances

diff -r 33840a854e63 -r b944ef973109 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);