diff -r 4b0ad6c5d1ca -r 0a8a75e400da src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Apr 28 11:47:01 2016 +0200
@@ -20,7 +20,7 @@
   for A :: "'a set set"
 where
   empty: "{} \<in> tiling A"
-| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
+| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
 
 
 text \<open>The union of two disjoint tilings is a tiling.\<close>