src/Pure/System/options.scala

       val ops =
         parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match {
           case Success(result, _) => result
           case bad => error(bad.toString)
         }
-      try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
+      try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } }
       catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) }
     }
 
     def parse_prefs(options: Options, content: String): Options =
       parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry)

     var options = empty
     for {
       dir <- Isabelle_System.components()
       file = dir + OPTIONS if file.is_file
     } { options = Parser.parse_file(options, file.implode, File.read(file)) }
-    (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _)
+    opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _)
   }
 
 
   /* encode */
 

     val options =
     {
       val options0 = Options.init()
       val options1 =
         if (build_options)
-          (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+          Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
         else options0
-      (options1 /: more_options)(_ + _)
+      more_options.foldLeft(options1)(_ + _)
     }
 
     if (get_option != "")
       Output.writeln(options.check_name(get_option).value, stdout = true)
 

       case i => this + (str.substring(0, i), str.substring(i + 1))
     }
   }
 
   def ++ (specs: List[Options.Spec]): Options =
-    (this /: specs)({ case (x, (y, z)) => x + (y, z) })
+    specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }
 
 
   /* sections */
 
   def set_section(new_section: String): Options =