diff -r efeebcfaef85 -r f84a93f1de2f src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Feb 15 08:36:19 2021 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Feb 19 11:52:34 2021 +0100
@@ -32,6 +32,7 @@
   val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string
   val get_int_setting : (string * string) list -> string * int -> int
+  val get_bool_setting : (string * string) list -> string * bool -> bool
   val cpu_time : ('a -> 'b) -> 'a -> 'b * int
 end
 
@@ -209,6 +210,12 @@
   | SOME NONE => error ("bad option: " ^ key)
   | NONE => default)
 
+fun get_bool_setting settings (key, default) =
+  (case Option.map Bool.fromString (AList.lookup (op =) settings key) of
+    SOME (SOME i) => i
+  | SOME NONE => error ("bad option: " ^ key)
+  | NONE => default)
+
 fun cpu_time f x =
   let val ({cpu, ...}, y) = Timing.timing f x
   in (y, Time.toMilliseconds cpu) end