# HG changeset patch
# User huffman
# Date 1257211774 28800
# Node ID 7c4ab69a15c38a72b292e84688ce30fdb3357b0f
# Parent  768b2bb9e66ab7597f603ca3d19bbf7de46aed45
define cprod_fun using Pair instead of cpair

diff -r 768b2bb9e66a -r 7c4ab69a15c3 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Mon Nov 02 17:19:49 2009 -0800
+++ b/src/HOLCF/Domain.thy	Mon Nov 02 17:29:34 2009 -0800
@@ -222,7 +222,7 @@
 definition
   cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
 where
-  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. <f\<cdot>x, g\<cdot>y>))"
+  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
 
 definition
   u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"