--- a/src/HOL/Library/old_recdef.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Sun Sep 06 22:14:51 2015 +0200
@@ -551,7 +551,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+ Const(@{const_name uncurry}, (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 case_prod} then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
else raise Match)
in
fun dest_pabs used tm =