# HG changeset patch
# User wenzelm
# Date 1439994070 -7200
# Node ID 5f3d6e16ea7890e0593535a30eb22505909185d3
# Parent  d94f3afd69b6dcead0fd6bf11f99f79234ac8a97
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;

diff -r d94f3afd69b6 -r 5f3d6e16ea78 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 19 16:21:10 2015 +0200
@@ -291,7 +291,8 @@
     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" ^