# HG changeset patch
# User wenzelm
# Date 1167418252 -3600
# Node ID e97fd6480091b909bb8942d1ba59fa6e94a723ce
# Parent  046e0482f0a100f48cde2a2cc1d831adb4801901
removed obsolete cond_add_path;

diff -r 046e0482f0a1 -r e97fd6480091 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Dec 29 19:50:51 2006 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Dec 29 19:50:52 2006 +0100
@@ -19,7 +19,6 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
-  val cond_add_path: Path.T -> ('a -> 'b) -> 'a -> 'b
   val ml_exts: string list
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
@@ -57,9 +56,6 @@
 fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
 fun with_path s f x = with_paths [s] f x;
 
-fun cond_add_path path f x =
-  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
-
 
 (* file formats *)
 
@@ -118,6 +114,9 @@
     | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
   end;
 
+fun cond_add_path path f x =
+  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
+
 in
 
 fun check_thy dir name ml = Master (cond_add_path dir check_thy_aux (name, ml));