diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Jan 13 00:45:28 2010 +0100
@@ -108,6 +108,7 @@
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_o[THEN eq_reflection]
+  id_def[symmetric, THEN eq_reflection]
   o_id[THEN eq_reflection]
   eq_comp_r