diff -r 361521bc7c47 -r 3fc2f9c40759 Prod.thy
--- a/Prod.thy	Thu Aug 18 12:23:52 1994 +0200
+++ b/Prod.thy	Thu Aug 18 12:38:12 1994 +0200
@@ -27,7 +27,7 @@
   Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
   fst	   :: "'a * 'b => 'a"
   snd	   :: "'a * 'b => 'b"
-  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
+  split    :: "[['a,'b]=>'c, 'a * 'b] => 'c"
   prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
   Pair	   :: "['a,'b] => 'a * 'b"
   "@Tuple" :: "args => 'a*'b"			("(1<_>)")
@@ -56,8 +56,8 @@
   Pair_def         "Pair(a,b) == Abs_Prod(Pair_Rep(a,b))"
   fst_def          "fst(p) == @a. ? b. p = <a,b>"
   snd_def          "snd(p) == @b. ? a. p = <a,b>"
-  split_def        "split(p,c) == c(fst(p),snd(p))"
-  prod_fun_def     "prod_fun(f,g) == (%z.split(z, %x y.<f(x), g(y)>))"
+  split_def        "split(c,p) == c(fst(p),snd(p))"
+  prod_fun_def     "prod_fun(f,g) == split(%x y.<f(x), g(y)>)"
   Sigma_def        "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
 
   Unit_def         "Unit == {p. p=True}"