replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
authorwenzelm
Sat, 15 Sep 2007 19:26:28 +0200
changeset 24583 d77e4d48e497
parent 24582 57599da58045
child 24584 01e83ffa6c54
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
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;