| changeset 21911 | e29bcab0c81c |
| parent 21871 | 9ce66839d9f1 |
| child 22483 | 86064f2f2188 |
--- a/src/HOL/Library/Char_ord.thy Wed Dec 27 19:09:59 2006 +0100 +++ b/src/HOL/Library/Char_ord.thy Wed Dec 27 19:10:00 2006 +0100 @@ -98,6 +98,7 @@ code_const char_to_int_pair (SML "raise/ Fail/ \"char'_to'_int'_pair\"") + (OCaml "failwith \"char'_to'_int'_pair\"") (Haskell "error/ \"char'_to'_int'_pair\"") end