--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 10:25:17 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 13:57:19 2010 +0100
@@ -51,7 +51,8 @@
theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
nitpick [card room = 1, card guest = 2, card "guest option" = 3,
- card key = 4, card state = 6, expect = genuine]
+ card key = 4, card state = 6, show_consts, format = 2,
+ expect = genuine]
(* nitpick [card room = 1, card guest = 2, expect = genuine] *)
oops