diff -r b7c3f264f8ac -r a24f7e5ee7ef src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sun Mar 26 22:31:11 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy	Mon Mar 27 16:25:53 2000 +0200
@@ -24,9 +24,9 @@
 
 constdefs
   below   :: "nat => nat set"
-   "below n    == {i. i<n}"
+   "below n   == {i. i<n}"
   
-  colored  :: "[nat, (nat*nat)set] => (nat*nat)set"
-   "colored b A == A Int {(i,j). (i+j) mod 2 = b}"
+  colored  :: "nat => (nat*nat)set"
+   "colored b == {(i,j). (i+j) mod 2 = b}"
 
 end