# HG changeset patch
# User wenzelm
# Date 1187365773 -7200
# Node ID 434c9fbc1787fe70a0b3e03b5fa0fabf7027afee
# Parent  7798a0f37253fabbaa17c5d560a2ecb3041bcdde
check_deps: ensure that theory is actually present, not just update_time > 1;

diff -r 7798a0f37253 -r 434c9fbc1787 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 17 13:59:00 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 17 17:49:33 2007 +0200
@@ -404,7 +404,8 @@
         else
           let
             val files' = map (check_ml master') files;
-            val current = update_time >= 0 andalso forall (is_some o snd) files';
+            val current = update_time >= 0 andalso can get_theory name
+              andalso forall (is_some o snd) files';
             val update_time' = if current then update_time else ~1;
             val text' = if current then text else explode (File.read thy_path);
             val deps' = SOME (make_deps update_time' master' text' parents files');