--- a/quotient.ML	Thu Nov 12 02:54:40 2009 +0100
+++ b/quotient.ML	Thu Nov 12 12:07:33 2009 +0100
@@ -146,7 +146,8 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (Binding.str_of qty_name) 
+  val qty_str = fst (dest_Type abs_ty)		  
+  val lthy3 = quotdata_update qty_str 
                                 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)