src/Pure/Thy/read.ML

                       let val thy = get_thyinfo t
                       in if is_some thy then
                              let val ThyInfo {children, ...} = the thy
                              in children union (next_level ts)
                              end
-                         else []
+                         else next_level ts
                       end
                   | next_level [] = [];
                   
                 val children = next_level thys
             in load_order children ((result \\ children) @ children) end;