src/HOL/Library/old_recdef.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 61466 9a468c3a1fa1
     1.1 --- a/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -551,7 +551,7 @@
     1.4  
     1.5  local
     1.6  fun mk_uncurry (xt, yt, zt) =
     1.7 -    Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
     1.8 +    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
     1.9  fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
    1.10    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
    1.11  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
    1.12 @@ -631,7 +631,7 @@
    1.13    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
    1.14  
    1.15  
    1.16 -local  fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
    1.17 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
    1.18                         else raise Match)
    1.19  in
    1.20  fun dest_pabs used tm =