--- a/src/Pure/ML/ml_init.ML Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/ML/ml_init.ML Wed Sep 06 20:51:28 2023 +0200
@@ -19,8 +19,6 @@
val error_depth = PolyML.error_depth;
-open Thread;
-
datatype illegal = Interrupt;
structure Basic_Exn: BASIC_EXN = Exn;