# HG changeset patch
# User wenzelm
# Date 995201248 -7200
# Node ID 4988fd27d6e6d9a6353bba024fdba0d24b7dfc78
# Parent  aa0571fb96b9235d98f04f87080c6f5b71a9800e
tuned;

diff -r aa0571fb96b9 -r 4988fd27d6e6 src/HOL/Product_Type.thy
--- 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"