# HG changeset patch
# User wenzelm
# Date 1749928029 -7200
# Node ID e09e986731e9dd419548a599e86a665ba20f9f86
# Parent  1008b8e7c78d1131d97d9364fb6de992015ab6ef
discontinue unused parameter (better done as system option);

diff -r 1008b8e7c78d -r e09e986731e9 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sat Jun 14 17:10:18 2025 +0200
+++ b/src/Pure/Build/store.scala	Sat Jun 14 21:07:09 2025 +0200
@@ -14,9 +14,8 @@
   def apply(
     options: Options,
     build_cluster: Boolean = false,
-    cache: Term.Cache = Term.Cache.make(),
-    other_ml_platform: Option[String] = None
-  ): Store = new Store(options, build_cluster, cache, other_ml_platform)
+    cache: Term.Cache = Term.Cache.make()
+  ): Store = new Store(options, build_cluster, cache)
 
 
   /* file names */
@@ -278,8 +277,7 @@
 class Store private(
     val options: Options,
     val build_cluster: Boolean,
-    val cache: Term.Cache,
-    other_ml_platform: Option[String]
+    val cache: Term.Cache
   ) {
   store =>
 
@@ -289,7 +287,7 @@
   /* ML system */
 
   def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM")
-  def ml_platform: String = other_ml_platform getOrElse Isabelle_System.getenv_strict("ML_PLATFORM")
+  def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM")
   def ml_identifier: String = ml_system + "_" + ml_platform