--- 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))