# HG changeset patch
# User wenzelm
# Date 961612705 -7200
# Node ID ef56f093259d8bb62cfe045b9ed3fc43e7adedb4
# Parent  c7ba07e3bbe8681a7ec309498ed5b36180021803
added with_paths;

diff -r c7ba07e3bbe8 -r ef56f093259d src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Jun 21 18:14:28 2000 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Jun 21 20:38:25 2000 +0200
@@ -12,6 +12,7 @@
   val add_path: string -> unit
   val del_path: string -> unit
   val with_path: string -> ('a -> 'b) -> 'a -> 'b
+  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
   val reset_path: unit -> unit
 end;
 
@@ -52,6 +53,7 @@
 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
 fun reset_path () = load_path := [Path.current];
 fun with_path s f x = Library.setmp load_path (Path.unpack s :: ! load_path) f x;
+fun with_paths ss f x = Library.setmp load_path (map Path.unpack ss @ ! load_path) f x;
 
 fun cond_with_path path f x =
   if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;