src/Pure/Syntax/lexicon.ML

 local
 
 val scan_vname =
   let
     fun nat n [] = n
-      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
+      | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs;
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
       | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =

 
 (* read_num: hex/bin/decimal *)
 
 local
 
-val ten = ord "0" + 10;
-val a = ord "a";
-val A = ord "A";
+val ten = Char.ord #"0" + 10;
+val a = Char.ord #"a";
+val A = Char.ord #"A";
 val _ = a > A orelse raise Fail "Bad ASCII";
 
 fun remap_hex c =
   let val x = ord c in
     if x >= a then chr (x - a + ten)