--- 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));