diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/file_format.scala Thu Mar 04 15:41:46 2021 +0100 @@ -39,7 +39,7 @@ agents.mkString("File_Format.Session(", ", ", ")") def prover_options(options: Options): Options = - (options /: agents)({ case (opts, agent) => agent.prover_options(opts) }) + agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) } def stop_session: Unit = agents.foreach(_.stop) }