add_path: del_path first;
authorwenzelm
Mon Aug 28 14:09:12 2000 +0200 (2000-08-28)
changeset 96965c8acc0282c8
parent 9695 ec7d7f877712
child 9697 c5fc121c2067
add_path: del_path first;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Mon Aug 28 13:52:38 2000 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Aug 28 14:09:12 2000 +0200
     1.3 @@ -49,8 +49,8 @@
     1.4  fun change_path f = load_path := f (! load_path);
     1.5  
     1.6  fun show_path () = map Path.pack (! load_path);
     1.7 -fun add_path s = change_path (cons (Path.unpack s));
     1.8  fun del_path s = change_path (filter_out (equal (Path.unpack s)));
     1.9 +fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
    1.10  fun reset_path () = load_path := [Path.current];
    1.11  fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
    1.12  fun with_path s f x = with_paths [s] f x;