removed obsolete cond_add_path;
authorwenzelm
Fri Dec 29 19:50:52 2006 +0100 (2006-12-29)
changeset 21950e97fd6480091
parent 21949 046e0482f0a1
child 21951 56abe5f3c612
removed obsolete cond_add_path;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Fri Dec 29 19:50:51 2006 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Dec 29 19:50:52 2006 +0100
     1.3 @@ -19,7 +19,6 @@
     1.4  signature THY_LOAD =
     1.5  sig
     1.6    include BASIC_THY_LOAD
     1.7 -  val cond_add_path: Path.T -> ('a -> 'b) -> 'a -> 'b
     1.8    val ml_exts: string list
     1.9    val ml_path: string -> Path.T
    1.10    val thy_path: string -> Path.T
    1.11 @@ -57,9 +56,6 @@
    1.12  fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
    1.13  fun with_path s f x = with_paths [s] f x;
    1.14  
    1.15 -fun cond_add_path path f x =
    1.16 -  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    1.17 -
    1.18  
    1.19  (* file formats *)
    1.20  
    1.21 @@ -118,6 +114,9 @@
    1.22      | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
    1.23    end;
    1.24  
    1.25 +fun cond_add_path path f x =
    1.26 +  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    1.27 +
    1.28  in
    1.29  
    1.30  fun check_thy dir name ml = Master (cond_add_path dir check_thy_aux (name, ml));