fixed a bug in update/next_level which occured when a child wasn't loaded

--- a/src/Pure/Thy/read.ML	Tue Dec 21 16:40:01 1993 +0100
+++ b/src/Pure/Thy/read.ML	Wed Dec 22 19:01:27 1993 +0100
@@ -296,7 +296,7 @@
                              let val ThyInfo {children, ...} = the thy
                              in children union (next_level ts)
                              end
-                         else []
+                         else next_level ts
                       end
                   | next_level [] = [];