src/Pure/Thy/latex.ML

   "`" => "{\\isacharbackquote}" |
   "{" => "{\\isacharbraceleft}" |
   "|" => "{\\isacharbar}" |
   "}" => "{\\isacharbraceright}" |
   "~" => "{\\isachartilde}" |
-  c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
+  c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
 
 val output_chrs = translate_string output_chr;
 
 fun output_known_sym (known_sym, known_ctrl) sym =
   (case Symbol.decode sym of