# HG changeset patch
# User wenzelm
# Date 1185032439 -7200
# Node ID 739707039b0d1fbad0e9994163a8d76297122bd3
# Parent  4127c1d910f15ce83e362d9e2944797c99bdec35
tuned;

diff -r 4127c1d910f1 -r 739707039b0d src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Jul 21 09:14:16 2007 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sat Jul 21 17:40:39 2007 +0200
@@ -66,6 +66,9 @@
 
 (* check files *)
 
+fun search_path dir path =
+  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
+
 fun check_ext exts dir src_path =
   let
     val path = Path.expand src_path;
@@ -75,11 +78,7 @@
       let val ext_path = Path.expand (Path.ext ext rel_path)
       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
-  in
-    (case get_first try_prfx (if Path.is_basic path then (! load_path) else [Path.current]) of
-      NONE => try_prfx dir
-    | res => res)
-  end;
+  in get_first try_prfx (search_path dir path) end;
 
 val check_file = check_ext [];
 val check_ml = check_ext ml_exts;
@@ -88,7 +87,7 @@
   let val thy_file = thy_path name in
     (case check_file dir thy_file of
       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
-        " in " ^ commas_quote (map Path.implode (dir :: ! load_path)))  (* FIXME imprecise *)
+        " in " ^ commas_quote (map Path.implode (search_path dir thy_file)))
     | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
   end;