src/HOL/List.thy

   [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
 and gen_list aG i = gen_list' aG i i;
 *}
   "char" ("string")
 attach (term_of) {*
-val term_of_char = HOLogic.mk_char;
+val term_of_char = HOLogic.mk_char o ord;
 *}
 attach (test) {*
 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
 *}