diff -r 0ae9d9e66cb7 -r 7d3d86beacd6 quotient.ML
--- a/quotient.ML	Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient.ML	Fri Nov 20 13:03:01 2009 +0100
@@ -146,10 +146,10 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* 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 qty_str = fst (Term.dest_Type abs_ty)
+  val _ = tracing ("storing under: " ^ qty_str)
+  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))