# HG changeset patch
# User wenzelm
# Date 1189877188 -7200
# Node ID d77e4d48e497230fcaa943560754d696906100c3
# Parent  57599da58045b686d038a8c0dabcc69f1c3114ad
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;

diff -r 57599da58045 -r d77e4d48e497 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Sep 15 19:26:17 2007 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Sep 15 19:26:28 2007 +0200
@@ -93,7 +93,7 @@
 
 val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
 val scan_digits1 = Scan.many1 Symbol.is_digit;
-val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
+val scan_hex1 = Scan.many1 Symbol.is_ascii_hex;
 val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
 
 val scan_id = scan_letter_letdigs >> implode;