--- a/src/HOL/ex/Mutil.thy	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/ex/Mutil.thy	Fri Jan 17 11:09:19 1997 +0100
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
 
 defs
   below_def  "below n    == nat_rec {} insert n"