src/HOL/Product_Type.thy
changeset 37387 3581483cca6c
parent 37278 307845cc7f51
child 37389 09467cdfa198
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jun 08 07:45:39 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jun 08 16:37:19 2010 +0200
     1.3 @@ -788,11 +788,8 @@
     1.4  
     1.5  subsubsection {* Derived operations *}
     1.6  
     1.7 -global consts
     1.8 -  curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
     1.9 -
    1.10 -local defs
    1.11 -  curry_def:    "curry == (%c x y. c (Pair x y))"
    1.12 +definition curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
    1.13 +  "curry = (\<lambda>c x y. c (x, y))"
    1.14  
    1.15  lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
    1.16    by (simp add: curry_def)