src/HOL/Library/old_recdef.ML

 
 fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
 
 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
 in
 fun mk_pabs{varstruct,body} =

 
 fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   | 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 =
    let val ({Bvar,Body}, used') = dest_abs used tm
    in {varstruct = Bvar, body = Body, used = used'}