src/Pure/System/session.ML

       val _ =
         init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants)
           parent ("Unsorted", name) doc_dump verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
-    in ignore (Par_Exn.release_all [res1, res2]) end)
+      val _ = ignore (Par_Exn.release_all [res1, res2]);
+      val _ = Options.reset_default ();
+    in () end)
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
     |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
     |> Unsynchronized.setmp Multithreading.trace trace_threads