--- a/src/HOL/Product_Type.thy Fri Nov 30 20:13:03 2007 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 30 20:13:05 2007 +0100
@@ -771,12 +771,11 @@
Setup of internal @{text split_rule}.
*}
-constdefs
- internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
+definition
+ internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
+where
"internal_split == split"
-lemmas [code func del] = internal_split_def
-
lemma internal_split_conv: "internal_split c (a, b) = c a b"
by (simp only: internal_split_def split_conv)