tuned signature;

--- a/src/Pure/Tools/dump.scala	Sat Nov 23 09:56:11 2019 +0000
+++ b/src/Pure/Tools/dump.scala	Sun Nov 24 15:31:28 2019 +0100
@@ -170,19 +170,16 @@
 
       def make_session(
         selected_sessions: List[String],
-        pure: Boolean = false,
+        session_logic: String = logic,
         record_proofs: Boolean = false): List[Session] =
       {
         if (selected_sessions.isEmpty) Nil
-        else {
-          val session_logic = if (pure) isabelle.Thy_Header.PURE else logic
-          List(new Session(context, session_logic, log, selected_sessions, record_proofs))
-        }
+        else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
       }
 
       val base =
         if (logic == isabelle.Thy_Header.PURE) Nil
-        else make_session(base_sessions, pure = true)
+        else make_session(base_sessions, session_logic = isabelle.Thy_Header.PURE)
 
       val main =
         make_session(
@@ -192,7 +189,7 @@
             proof_sessions.contains(name)))
 
       val proofs =
-        make_session(proof_sessions, pure = true, record_proofs = true)
+        make_session(proof_sessions, session_logic = isabelle.Thy_Header.PURE, record_proofs = true)
 
       val afp =
         if (afp_sessions.isEmpty) Nil