# HG changeset patch
# User clasohm
# Date 756583287 -3600
# Node ID b9f087b42a4445c9c5af1a2f791df546f129e864
# Parent  4a213aaca3d9faad8e48dda16f8fd1737b696e92
fixed a bug in update/next_level which occured when a child wasn't loaded

diff -r 4a213aaca3d9 -r b9f087b42a44 src/Pure/Thy/read.ML
--- 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 [] = [];