# HG changeset patch
# User wenzelm
# Date 1535993103 -7200
# Node ID cca4555f412d2d157b69d2ac6852c695c6dae595
# Parent  1dbdad1b57a505e23b46cd59652d25649c04cf78
tuned;

diff -r 1dbdad1b57a5 -r cca4555f412d src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 03 16:23:26 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 03 18:45:03 2018 +0200
@@ -79,8 +79,10 @@
   val default_output_dir = Path.explode("dump")
 
   def make_options(options: Options, aspects: List[Aspect]): Options =
-    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
-      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+  {
+    val options1 = options + "completion_limit=0" + "ML_statistics=false"
+    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+  }
 
   def dump(options: Options, logic: String,
     aspects: List[Aspect] = Nil,