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