--- a/Quot/QuotSum.thy	Tue Jan 26 08:09:22 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 08:55:55 2010 +0100
@@ -76,17 +76,15 @@
   apply(blast)+
   done
 
-lemma sum_map_id[id_simps]: 
-  shows "sum_map id id \<equiv> id"
-  apply (rule eq_reflection)
+lemma sum_map_id[id_simps]:
+  shows "sum_map id id = id"
   apply (rule ext)
   apply (case_tac x)
   apply (auto)
   done
 
-lemma sum_rel_eq[id_simps]: 
-  "sum_rel op = op = \<equiv> op ="
-  apply (rule eq_reflection)
+lemma sum_rel_eq[id_simps]:
+  "(sum_rel op = op =) = op ="
   apply (rule ext)+
   apply (case_tac x)
   apply auto