# HG changeset patch
# User wenzelm
# Date 967464552 -7200
# Node ID 5c8acc0282c85b363f6a658372650403675f6f44
# Parent  ec7d7f87771229942605a7c65c7913091946d511
add_path: del_path first;

diff -r ec7d7f877712 -r 5c8acc0282c8 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Aug 28 13:52:38 2000 +0200
+++ b/src/Pure/Thy/thy_load.ML	Mon Aug 28 14:09:12 2000 +0200
@@ -49,8 +49,8 @@
 fun change_path f = load_path := f (! load_path);
 
 fun show_path () = map Path.pack (! load_path);
-fun add_path s = change_path (cons (Path.unpack s));
 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
+fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
 fun reset_path () = load_path := [Path.current];
 fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
 fun with_path s f x = with_paths [s] f x;