tuned proof in order to avoid warning message

--- a/src/HOL/Library/Quotient_Product.thy	Mon Apr 02 16:07:24 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Mon Apr 02 18:12:53 2012 +0100
@@ -85,7 +85,8 @@
 
 lemma split_rsp [quot_respect]:
   shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
-  by (auto intro!: fun_relI elim!: fun_relE)
+  unfolding prod_rel_def fun_rel_def
+  by auto
 
 lemma split_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"