--- a/quotient.ML	Wed Oct 28 10:29:00 2009 +0100
+++ b/quotient.ML	Wed Oct 28 15:25:11 2009 +0100
@@ -10,7 +10,8 @@
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
-  val quotdata_lookup: theory -> quotient_info list
+  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
 end;
@@ -70,7 +71,8 @@
    val extend = I
    fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
 
-val quotdata_lookup = QuotData.get
+val quotdata_lookup_thy = QuotData.get
+val quotdata_lookup = QuotData.get 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