--- a/quotient_info.ML	Thu Nov 12 02:18:36 2009 +0100
+++ b/quotient_info.ML	Thu Nov 12 02:54:40 2009 +0100
@@ -7,10 +7,10 @@
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
   val print_quotinfo: Proof.context -> unit
-  val quotdata_lookup_thy: theory -> quotient_info list
-  val quotdata_lookup: Proof.context -> quotient_info list
-  val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
-  val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
+  val quotdata_lookup_thy: theory -> string -> quotient_info option
+  val quotdata_lookup: Proof.context -> string -> quotient_info option
+  val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
+  val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
   type qenv = (typ * typ) list
   val mk_qenv: Proof.context -> qenv
@@ -41,7 +41,6 @@
 
 val maps_lookup = Symtab.lookup o MapsData.get
 
-
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
 
@@ -74,19 +73,19 @@
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
-  (type T = quotient_info list
-   val empty = []
+  (type T = quotient_info Symtab.table
+   val empty = Symtab.empty
    val extend = I
-   val merge = (op @)) (* FIXME: is this the correct merging function for the list? *)
+   val merge = Symtab.merge (K true)) 
 
-val quotdata_lookup_thy = QuotData.get
-val quotdata_lookup = QuotData.get o ProofContext.theory_of
+val quotdata_lookup_thy = Symtab.lookup o QuotData.get
+val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
-fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
-      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy
+fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = 
+      QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
 
-fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
+fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
+      ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
 fun print_quotinfo ctxt =
 let
@@ -102,7 +101,8 @@
            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
-  |> map prt_quot
+  |> Symtab.dest
+  |> map (prt_quot o snd)
   |> Pretty.big_list "quotients:" 
   |> Pretty.writeln
 end
@@ -117,7 +117,8 @@
 
 fun mk_qenv ctxt =
 let
-  val qinfo = quotdata_lookup ctxt
+  val thy = ProofContext.theory_of ctxt
+  val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd
 in
   map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
 end