src/Pure/ML/ml_settings.scala
changeset 82718 e1a8753eaad7
parent 82716 6e33d46b1400
child 82720 956ecf2c07a0
--- a/src/Pure/ML/ml_settings.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -8,13 +8,11 @@
 
 
 object ML_Settings {
-  def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): System =
-    new System(env)
-
-  class System(env: Isabelle_System.Settings = Isabelle_System.Settings()) extends ML_Settings {
-    override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
-    override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
-  }
+  def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): ML_Settings =
+    new ML_Settings {
+      override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
+      override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
+    }
 }
 
 trait ML_Settings {