diff -r 5455b19ef138 -r 8d51795ef54d Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Mon Jan 25 20:35:42 2010 +0100
+++ b/Quot/QuotProd.thy	Mon Jan 25 20:47:20 2010 +0100
@@ -80,7 +80,7 @@
      (simp add: prod_fun_def)
 
 lemma prod_rel_eq[id_simps]: 
-  shows "prod_rel op = op = \<equiv> op ="
+  shows "prod_rel (op =) (op =) \<equiv> (op =)"
   apply (rule eq_reflection)
   apply (rule ext)+
   apply auto