* Theory loader: old-style ML proof scripts being *attached* to a thy file (with the same base name as the theory) are considered a legacy feature, which will disappear eventually. Even now, the theory loader no longer maintains dependencies on such files.