# HG changeset patch
# User wenzelm
# Date 1279824405 -7200
# Node ID 445e5a3244cc7b03128c27f5468aae26cc472c51
# Parent  9e482a3e651e0846137fa1e2d0507f744f1b743c
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
reset_path is CRITICAL;

diff -r 9e482a3e651e -r 445e5a3244cc src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Jul 22 20:36:41 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Jul 22 20:46:45 2010 +0200
@@ -10,8 +10,6 @@
   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
   val reset_path: unit -> unit
 end;
 
@@ -50,13 +48,7 @@
   CRITICAL (fn () =>
     (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
 
-fun reset_path () = load_path := [Path.current];
-
-fun with_paths ss f x =
-  CRITICAL (fn () =>
-    setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
-
-fun with_path s f x = with_paths [s] f x;
+fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
 
 fun search_path dir path =
   distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));