diff -r 0ff855a6ffb7 -r ce774af6b964 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Jan 26 12:06:47 2010 +0100
+++ b/Quot/QuotMain.thy	Tue Jan 26 12:24:23 2010 +0100
@@ -112,7 +112,7 @@
 lemmas [id_simps] =
   id_def[symmetric]
   fun_map_id
-  id_apply[THEN eq_reflection]
+  id_apply
   id_o
   o_id
   eq_comp_r