--- 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 [] = [];