| changeset 23802 | cd09234405b6 |
| parent 23784 | 75e6b9dd5336 |
| child 24245 | 4ffeb1dd048a |
--- a/src/Pure/Syntax/lexicon.ML Thu Jul 12 00:15:39 2007 +0200 +++ b/src/Pure/Syntax/lexicon.ML Thu Jul 12 00:15:41 2007 +0200 @@ -379,7 +379,7 @@ val ten = ord "0" + 10; val a = ord "a"; val A = ord "A"; -val _ = a > A orelse error "Bad ASCII"; +val _ = a > A orelse sys_error "Bad ASCII"; fun remap_hex c = let val x = ord c in