diff -r 5455b19ef138 -r 8d51795ef54d Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Jan 25 20:35:42 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 25 20:47:20 2010 +0100
@@ -111,7 +111,7 @@
 
 text {* Lemmas about simplifying id's. *}
 lemmas [id_simps] =
-  id_def[symmetric, THEN eq_reflection]
+  id_def[symmetric]
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_o[THEN eq_reflection]