diff -r c46b3f9f79ea -r 53d0fb1359d4 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Jan 13 11:42:30 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Jan 13 11:59:42 2018 +0100
@@ -44,7 +44,7 @@
 "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
  s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
    roomk := (roomk s)(r := k'),
-   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<comment> \<open>\<open>\<and> k' = currk s r\<close>\<close>
+   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<^cancel>\<open>\<and> k' = currk s r\<close>
                          \<or> safe s r)\<rparr> \<in> reach" |
 exit_room:
 "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"