# HG changeset patch
# User wenzelm
# Date 966682106 -7200
# Node ID 896f5c5cfc560ab6373508b165d4f7ff22744dc4
# Parent  8b3ab0244560c37d7f827dd70571cee6efd25d2c
cond_add_path;

diff -r 8b3ab0244560 -r 896f5c5cfc56 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sat Aug 19 12:47:16 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sat Aug 19 12:48:26 2000 +0200
@@ -152,7 +152,7 @@
   | None => "");
 
 fun try_update_thy_only file =
-  ThyLoad.cond_with_path (Path.dir (Path.unpack file)) (fn () =>
+  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
     let val name = thy_name file in
       if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
       else warning ("Unkown theory context of ML file." ^ which_context ())