1.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -13,8 +13,6 @@
     1.4  where
     1.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
     1.6  
     1.7 -declare [[map prod = prod_rel]]
     1.8 -
     1.9  lemma prod_rel_apply [simp]:
    1.10    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.11    by (simp add: prod_rel_def)
    1.12 @@ -45,6 +43,8 @@
    1.13    apply (auto simp add: split_paired_all)
    1.14    done
    1.15  
    1.16 +declare [[map prod = (prod_rel, prod_quotient)]]
    1.17 +
    1.18  lemma Pair_rsp [quot_respect]:
    1.19    assumes q1: "Quotient R1 Abs1 Rep1"
    1.20    assumes q2: "Quotient R2 Abs2 Rep2"