src/HOL/Product_Type.thy
changeset 11425 4988fd27d6e6
parent 11032 83f723e86dac
child 11451 8abfb4f7bd02
--- 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"