--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 07 22:15:54 2018 +0100
@@ -725,7 +725,7 @@
Some x \<Rightarrow> Some x
| None \<Rightarrow> full_exhaustive_class.full_exhaustive
(\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
- (min (i - 1) 8) (* generate at most 8 bits *)
+ (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
else None)"
instance ..