tuned;

--- a/src/HOL/Product_Type.thy	Fri Jul 13 18:28:46 2001 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jul 15 14:47:28 2001 +0200
@@ -119,7 +119,7 @@
 use "Product_Type_lemmas.ML"
 
 constdefs
-  internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c"
+  internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
   "internal_split == split"
 
 lemma internal_split_conv: "internal_split c (a, b) = c a b"