diff -r a90e40118874 -r 2739631ac368 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 07 10:51:20 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 07 11:35:43 2019 +0200
@@ -88,7 +88,6 @@
     def apply(
       options: Options,
       logic: String,
-      dump_checkpoints: Boolean = false,
       aspects: List[Aspect] = Nil,
       progress: Progress = No_Progress,
       log: Logger = No_Logger,
@@ -96,15 +95,13 @@
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty): Session =
     {
-      new Session(
-        options, logic, dump_checkpoints, aspects, progress, log, dirs, select_dirs, selection)
+      new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
     }
   }
 
   class Session private(
     options: Options,
     logic: String,
-    dump_checkpoints: Boolean,
     aspects: List[Aspect],
     progress: Progress,
     log: Logger,
@@ -215,7 +212,6 @@
           session.use_theories(used_theories.map(_.theory),
             unicode_symbols = unicode_symbols,
             progress = progress,
-            checkpoints = if (dump_checkpoints) deps.dump_checkpoints else Set.empty,
             commit = Some(Consumer.apply _))
 
         val bad_theories = Consumer.shutdown()
@@ -247,7 +243,6 @@
   def dump(
     options: Options,
     logic: String,
-    dump_checkpoints: Boolean = false,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
     log: Logger = No_Logger,
@@ -257,9 +252,8 @@
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
     val session =
-      Session(options, logic, dump_checkpoints = dump_checkpoints, aspects = aspects,
-        progress = progress, log = log, dirs = dirs, select_dirs = select_dirs,
-        selection = selection)
+      Session(options, logic, aspects = aspects, progress = progress, log = log, dirs = dirs,
+        select_dirs = select_dirs, selection = selection)
 
     session.run((args: Args) =>
       {
@@ -280,7 +274,6 @@
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
-      var dump_checkpoints = false
       var output_dir = default_output_dir
       var requirements = false
       var exclude_session_groups: List[String] = Nil
@@ -298,7 +291,6 @@
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
-    -C           observe option dump_checkpoint for theories
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
@@ -316,7 +308,6 @@
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
-      "C" -> (_ => dump_checkpoints = true),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
@@ -335,7 +326,6 @@
 
       progress.interrupt_handler {
         dump(options, logic,
-          dump_checkpoints = dump_checkpoints,
           aspects = aspects,
           progress = progress,
           dirs = dirs,