--- a/Quot/QuotSum.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -84,15 +84,11 @@
   done
 
 lemma sum_map_id[id_simps]: 
-  shows "sum_map id id \<equiv> id"
-  apply (rule eq_reflection)
-  apply (simp add: expand_fun_eq split_sum_all)
-  done
+  shows "sum_map id id = id"
+  by (simp add: expand_fun_eq split_sum_all)
 
 lemma sum_rel_eq[id_simps]: 
-  shows "sum_rel (op =) (op =) \<equiv> (op =)"
-  apply (rule eq_reflection)
-  apply(simp add: expand_fun_eq split_sum_all)
-  done
+  shows "sum_rel (op =) (op =) = (op =)"
+  by (simp add: expand_fun_eq split_sum_all)
 
 end