diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Mutil.thy	Sat May 27 17:42:02 2006 +0200
@@ -30,16 +30,15 @@
 
 text {* \medskip Sets of squares of the given colour*}
 
-constdefs
+definition
   coloured :: "nat => (nat \<times> nat) set"
-   "coloured b == {(i, j). (i + j) mod 2 = b}"
+  "coloured b = {(i, j). (i + j) mod 2 = b}"
 
-syntax whites  :: "(nat \<times> nat) set"
-       blacks  :: "(nat \<times> nat) set"
-
-translations
-  "whites" == "coloured 0"
-  "blacks" == "coloured (Suc 0)"
+abbreviation
+  whites  :: "(nat \<times> nat) set"
+  "whites == coloured 0"
+  blacks  :: "(nat \<times> nat) set"
+  "blacks == coloured (Suc 0)"
 
 
 text {* \medskip The union of two disjoint tilings is a tiling *}