author | wenzelm |
Thu, 12 Jul 2007 00:15:41 +0200 | |
changeset 23802 | cd09234405b6 |
parent 23801 | 20c0dd4f783f |
child 23803 | 11bf7af10ec8 |
--- 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