# HG changeset patch
# User wenzelm
# Date 941036971 -7200
# Node ID 720af28e635490a84174a5a7a8624a3168894a1a
# Parent  7ad4dd78a9a7518a42e7c9155026d191a46d54c1
export cond_with_path;

diff -r 7ad4dd78a9a7 -r 720af28e6354 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Oct 27 17:09:05 1999 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Oct 27 17:09:31 1999 +0200
@@ -17,6 +17,7 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
+  val cond_with_path: Path.T -> ('a -> 'b) -> 'a -> 'b
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
   val check_file: Path.T -> (Path.T * File.info) option