# HG changeset patch
# User wenzelm
# Date 971904648 -7200
# Node ID dd46544e259d8cff085df6522ca5f3ff247a24af
# Parent  5cc44cae9590be5f7e8e37545a99acb01f3ff3ff
added path_add;

diff -r 5cc44cae9590 -r dd46544e259d src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Oct 18 23:29:49 2000 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Oct 18 23:30:48 2000 +0200
@@ -10,6 +10,7 @@
 sig
   val show_path: unit -> string list
   val add_path: string -> unit
+  val path_add: string -> unit
   val del_path: string -> unit
   val with_path: string -> ('a -> 'b) -> 'a -> 'b
   val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
@@ -51,6 +52,7 @@
 fun show_path () = map Path.pack (! load_path);
 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 path_add s = (del_path s; change_path (fn path => path @ [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;