changeset 24130 | 5ab8044b6d46 |
parent 24037 | 0a41d2ebc0cd |
child 24166 | 7b28dc69bdbb |
--- a/src/HOL/List.thy Thu Aug 02 17:29:40 2007 +0200 +++ b/src/HOL/List.thy Thu Aug 02 17:31:10 2007 +0200 @@ -2790,7 +2790,7 @@ *} "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")));