Repaired term_of_char.
authorberghofe
Thu Aug 02 17:31:10 2007 +0200 (2007-08-02)
changeset 241305ab8044b6d46
parent 24129 591394d9ee66
child 24131 1099f6c73649
Repaired term_of_char.
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Aug 02 17:29:40 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Aug 02 17:31:10 2007 +0200
     1.3 @@ -2790,7 +2790,7 @@
     1.4  *}
     1.5    "char" ("string")
     1.6  attach (term_of) {*
     1.7 -val term_of_char = HOLogic.mk_char;
     1.8 +val term_of_char = HOLogic.mk_char o ord;
     1.9  *}
    1.10  attach (test) {*
    1.11  fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));