diff -r c445b6aeefc9 -r 04ef4bd3b936 Quot/QuotOption.thy
--- a/Quot/QuotOption.thy	Tue Jan 26 07:14:10 2010 +0100
+++ b/Quot/QuotOption.thy	Tue Jan 26 07:42:52 2010 +0100
@@ -73,17 +73,15 @@
   apply(simp add: Quotient_abs_rep[OF q])
   done
 
-lemma option_map_id[id_simps]: 
-  shows "option_map id \<equiv> id"
-  apply (rule eq_reflection)
+lemma option_map_id[id_simps]:
+  shows "option_map id = id"
   apply (auto simp add: expand_fun_eq)
   apply (case_tac x)
   apply (auto)
   done
 
-lemma option_rel_eq[id_simps]: 
-  shows "option_rel (op =) \<equiv> (op =)"
-  apply(rule eq_reflection)
+lemma option_rel_eq[id_simps]:
+  shows "option_rel (op =) = (op =)"
   apply(auto simp add: expand_fun_eq)
   apply(case_tac x)
   apply(case_tac [!] xa)