diff --git a/src/Pure/Admin/check_sources.scala b/src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala
+++ b/src/Pure/Admin/check_sources.scala
@@ -1,74 +1,79 @@
 /*  Title:      Pure/Admin/check_sources.scala
     Author:     Makarius
 
 Some sanity checks for Isabelle sources.
 */
 
 package isabelle
 
 
 object Check_Sources
 {
   def check_file(path: Path)
   {
     val file_name = path.implode
     val file_pos = path.position
     def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
 
     if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
       Output.warning("Illegal file-name on Windows" + Position.here(file_pos))
 
-    val content = File.read(path)
+    val bytes = Bytes.read(path)
+    val content = bytes.text
+
+    if (Bytes(content) != bytes) {
+      Output.warning("Bad UTF8 encoding" + Position.here(file_pos))
+    }
 
     for { (line, i) <- split_lines(content).iterator.zipWithIndex }
     {
       try {
         Symbol.decode_strict(line)
 
         for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
         {
           Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
             Position.here(line_pos(i)))
         }
       }
       catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
 
       if (line.contains('\t'))
         Output.warning("TAB character" + Position.here(line_pos(i)))
     }
 
     if (content.contains('\r'))
       Output.warning("CR character" + Position.here(file_pos))
 
     if (Word.bidi_detect(content))
       Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
   }
 
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
     val hg = Mercurial.repository(root)
     for {
       file <- hg.known_files()
       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
     } check_file(root + Path.explode(file))
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
     {
       val getopts = Getopts("""
 Usage: isabelle check_sources [ROOT_DIRS...]
 
   Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
 """)
 
       val specs = getopts(args)
       if (specs.isEmpty) getopts.usage()
 
       for (root <- specs) check_hg(Path.explode(root))
     })
 }