diff -r 878bd5922f3b -r 6c05c4632949 src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat May 28 17:34:28 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat May 28 17:35:12 2016 +0200
@@ -109,9 +109,17 @@
 
 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
-where find_first'_code [code]:
-  "find_first' f [] = Quickcheck_Exhaustive.No_value"
-  "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
+where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
+  and find_first'_Cons: "find_first' f (x # xs) =
+    (case f (Quickcheck_Exhaustive.Known x) of
+      Quickcheck_Exhaustive.No_value => find_first' f xs
+    | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
+    | Quickcheck_Exhaustive.Unknown_value =>
+        (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
+          Quickcheck_Exhaustive.Value x
+        | _ => Quickcheck_Exhaustive.Unknown_value))"
+
+lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
 
 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"