--- a/quotient.ML	Fri Oct 30 19:03:53 2009 +0100
+++ b/quotient.ML	Mon Nov 02 09:33:48 2009 +0100
@@ -6,7 +6,7 @@
   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_lookup_thy: theory -> string -> maps_info option
   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
@@ -32,7 +32,9 @@
    val extend = I
    fun merge _ = Symtab.merge (K true))
 
-val maps_lookup = Symtab.lookup o MapsData.get
+val maps_lookup_thy = 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)
 
@@ -242,7 +244,7 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))