diff -r 28e312cfc806 -r 9a0e8ab42ee8 quotient.ML
--- a/quotient.ML	Mon Nov 23 22:00:54 2009 +0100
+++ b/quotient.ML	Mon Nov 23 23:09:03 2009 +0100
@@ -153,8 +153,12 @@
   (* storing the quot-info *)
   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  
+  val lthy3 = quotdata_update qty_str 
+               (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
+  (* FIXME: the relation needs to be a string, since its type needs *)
+  (* FIXME: to recalculated in for example REGULARIZE *)
+
   (* storing of the equiv_thm under a name *)
   val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3