1.1 --- a/src/Pure/Thy/thy_load.ML Fri Jul 20 19:13:07 2007 +0200
1.2 +++ b/src/Pure/Thy/thy_load.ML Fri Jul 20 19:54:03 2007 +0200
1.3 @@ -75,9 +75,11 @@
1.4 let val ext_path = Path.expand (Path.ext ext rel_path)
1.5 in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
1.6 fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
1.7 -
1.8 - val via_load_path = if Path.is_basic path then get_first try_prfx (! load_path) else NONE;
1.9 - in (case via_load_path of NONE => try_prfx dir | res => res) end;
1.10 + in
1.11 + (case get_first try_prfx (if Path.is_basic path then (! load_path) else [Path.current]) of
1.12 + NONE => try_prfx dir
1.13 + | res => res)
1.14 + end;
1.15
1.16 val check_file = check_ext [];
1.17 val check_ml = check_ext ml_exts;