--- a/Quot/QuotMain.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotMain.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -109,8 +109,8 @@
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection, symmetric]
   id_o[THEN eq_reflection]
-  o_id[THEN eq_reflection] 
-
+  o_id[THEN eq_reflection]
+  eq_comp_r
 
 (* The translation functions for the lifting process. *)
 use "quotient_term.ML"