--- a/quotient.ML	Sun Oct 18 10:34:53 2009 +0200
+++ b/quotient.ML	Tue Oct 20 00:12:05 2009 +0200
@@ -1,14 +1,40 @@
 signature QUOTIENT =
 sig
+  type maps_info = {mapfun: string, relfun: string}
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
+  val maps_lookup: theory -> string -> maps_info option
+  val maps_update: string -> maps_info -> theory -> theory                                  
+
 end;
 
 structure Quotient: QUOTIENT =
 struct
 
+(* data containers *)
+(*******************)
+
+(* map-functions and rel-functions *)
+type maps_info = {mapfun: string, relfun: string}
+
+local
+  structure Data = TheoryDataFun
+  (type T = maps_info Symtab.table
+   val empty = Symtab.empty
+   val copy = I
+   val extend = I
+   fun merge _ = Symtab.merge (K true))
+in
+  val maps_lookup = Symtab.lookup o Data.get
+  fun maps_update k v = Data.map (Symtab.update (k, v))
+end
+
+
+(* definition of the quotient type *)
+(***********************************)
+
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
@@ -167,6 +193,9 @@
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 
+
+
+
 (* interface and syntax setup *)
 
 (* the ML-interface takes a list of 4-tuples consisting of  *)
@@ -175,7 +204,7 @@
 (* - its mixfix annotation                                  *)
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
-  
+
 fun mk_quotient_type quot_list lthy = 
 let
   fun get_goal (rty, rel) =