diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -551,7 +551,7 @@
 
 local
 fun mk_uncurry (xt, yt, zt) =
-    Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
 fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
 fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -631,7 +631,7 @@
   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
 
 
-local  fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
+local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
                        else raise Match)
 in
 fun dest_pabs used tm =