diff -r 2e9a86203d59 -r 934a58983311 Prod.thy
--- a/Prod.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Prod.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -11,29 +11,32 @@
 *)
 
 Prod = Set +
+
 types   
-	"*"  2        (infixr 20)
-        unit
+  ('a,'b) "*"          (infixr 20)
+  unit
+
 arities 
-   "*"      :: (term,term)term
-   unit     :: term
+  "*"      :: (term,term)term
+  unit     :: term
+
 consts
-   Pair_Rep :: "['a,'b] => ['a,'b] => bool"
-   Prod	    :: "('a => 'b => bool)set"
-   Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
-   Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
-   fst	    :: "'a * 'b => 'a"
-   snd	    :: "'a * 'b => 'b"
-   split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
-   prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
-   Pair	    :: "['a,'b] => 'a * 'b"
-   "@Tuple" :: "args => 'a*'b"			("(1<_>)")
-   Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
+  Pair_Rep :: "['a,'b] => ['a,'b] => bool"
+  Prod	   :: "('a => 'b => bool)set"
+  Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
+  Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
+  fst	   :: "'a * 'b => 'a"
+  snd	   :: "'a * 'b => 'b"
+  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
+  prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
+  Pair	   :: "['a,'b] => 'a * 'b"
+  "@Tuple" :: "args => 'a*'b"			("(1<_>)")
+  Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
 
-   Unit	    :: "bool set"
-   Rep_Unit :: "unit => bool"
-   Abs_Unit :: "bool => unit"
-   Unity    :: "unit"					("<>")
+  Unit	   :: "bool set"
+  Rep_Unit :: "unit => bool"
+  Abs_Unit :: "bool => unit"
+  Unity    :: "unit"					("<>")
 
 translations