src/Pure/Thy/thy_info.ML

   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
     val node_name = File.full_path dir (Resources.thy_path path);
     fun check_entry (Task (node_name', _, _)) =
-          if node_name = node_name' then ()
+          if op = (apply2 File.platform_path (node_name, node_name'))
+          then ()
           else
             error ("Incoherent imports for theory " ^ quote name ^
               Position.here require_pos ^ ":\n" ^
               "  " ^ Path.print node_name ^ "\n" ^
               "  " ^ Path.print node_name')