diff -r 7af81ea081d6 -r 13ea9a34c269 quotient.ML
--- a/quotient.ML	Thu Nov 12 13:57:20 2009 +0100
+++ b/quotient.ML	Fri Nov 13 16:44:36 2009 +0100
@@ -149,7 +149,7 @@
   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
   (* FIXME: varifyT should not be used *)
-  (* the type name maybe should be calculated via qty_name and Sign.intern_type *} 
+  (* the type name maybe should be calculated via qty_name and Sign.intern_type *)
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))