# HG changeset patch
# User wenzelm
# Date 1280931111 -7200
# Node ID 2b08a96a283e4429697507c146552c1af2f21fa3
# Parent  a5916f2b6791ebb4d2c767791d14839054badbdf
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;

diff -r a5916f2b6791 -r 2b08a96a283e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:50:55 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 16:11:51 2010 +0200
@@ -238,8 +238,9 @@
     fun after_load' () =
      (after_load ();
       NAMED_CRITICAL "Thy_Info" (fn () =>
-        (change_thys (new_entry name parent_names (SOME deps, SOME theory));
-          perform Update name)));
+       (map get_theory parent_names;
+        change_thys (new_entry name parent_names (SOME deps, SOME theory));
+        perform Update name)));
 
   in (theory, after_load') end;