--- a/Quot/QuotProd.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotProd.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -90,6 +90,8 @@
   shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
 
+lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
+  by (rule eq_reflection) (simp add: prod_fun_def)
 
 section {* general setup for products *}