src/Pure/General/scan.ML

   | extend_lexicon lexicon chrss =
       let
         fun ext (lex, chrs) =
           let
             fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
-                  (case String.compare (c, d) of
+                  (case string_ord (c, d) of
                     LESS => Branch (d, a, add lt chs, eq, gt)
                   | EQUAL => Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
                   | GREATER => Branch (d, a, lt, eq, add gt chs))
               | add Empty [c] =
                   Branch (c, chrs, Empty, Empty, Empty)

 (* is_literal *)
 
 fun is_literal Empty _ = false
   | is_literal _ [] = false
   | is_literal (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
-      (case String.compare (c, d) of
+      (case string_ord (c, d) of
         LESS => is_literal lt chs
       | EQUAL => a <> no_literal andalso null cs orelse is_literal eq cs
       | GREATER => is_literal gt chs);
 
 

 fun literal lex chrs =
   let
     fun lit Empty res _ = res
       | lit (Branch _) _ [] = raise MORE NONE
       | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
-          (case String.compare (c, d) of
+          (case string_ord (c, d) of
             LESS => lit lt res chs
           | EQUAL => lit eq (if a = no_literal then res else SOME (a, cs)) cs
           | GREATER => lit gt res chs);
   in
     (case lit lex NONE chrs of