--- a/quotient.ML	Thu Nov 12 13:56:07 2009 +0100
+++ b/quotient.ML	Thu Nov 12 13:57:20 2009 +0100
@@ -147,8 +147,9 @@
 
   (* storing the quot-info *)
   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
+  val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  (* FIXME: varifyT should not be used *)
+  (* the type name maybe should be calculated via qty_name and Sign.intern_type *} 
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))