--- a/src/HOL/Product_Type.thy Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Product_Type.thy Tue Jun 08 16:37:19 2010 +0200
@@ -788,11 +788,8 @@
subsubsection {* Derived operations *}
-global consts
- curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
-
-local defs
- curry_def: "curry == (%c x y. c (Pair x y))"
+definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
+ "curry = (\<lambda>c x y. c (x, y))"
lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
by (simp add: curry_def)