src/Pure/General/symbol.ML

     if is_ascii_letter s then Letter
     else if is_ascii_digit s then Digit
     else if is_ascii_quasi s then Quasi
     else if is_ascii_blank s then Blank
     else if is_char s then Other
-    else getOpt (Symtab.lookup (symbol_kinds, s), Other);
+    else if_none (Symtab.lookup (symbol_kinds, s)) Other;
 end;
 
 fun is_letter s = kind s = Letter;
 fun is_digit s = kind s = Digit;
 fun is_quasi s = kind s = Quasi;

   | no_explode (_ :: cs) = no_explode cs;
 
 fun sym_explode str =
   let val chs = explode str in
     if no_explode chs then chs
-    else valOf (Scan.read stopper (Scan.repeat scan) chs)
+    else the (Scan.read stopper (Scan.repeat scan) chs)
   end;
 
 val chars_only = not o exists_string (equal "\\");