# HG changeset patch
# User wenzelm
# Date 1574605888 -3600
# Node ID 1c58a01a372e35e131aa9bfec446d21338c53cb4
# Parent  8bdf3c36011c1ffcf21e0a78c78d8e54438a4b34
tuned signature;

diff -r 8bdf3c36011c -r 1c58a01a372e src/Pure/Tools/dump.scala
--- 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