diff -r aa960d16570f -r b1f55dd64481 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotProd.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -46,7 +46,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
-apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2])
+apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2])
 apply(simp)
 done