diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -634,12 +634,12 @@
           end
       end
 
-  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
-     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
+  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
 
-  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
-     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
+  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
+     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
 
   | (t1 $ t2, t1' $ t2') =>