# HG changeset patch
# User wenzelm
# Date 1184192141 -7200
# Node ID cd09234405b67943307fbdd3252b31988766e19b
# Parent  20c0dd4f783f8b1d1be46020e49bf0ca8519c22b
sys_error;

diff -r 20c0dd4f783f -r cd09234405b6 src/Pure/Syntax/lexicon.ML
--- 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