--- a/src/Pure/Tools/simplifier_trace.ML Thu Apr 14 16:02:22 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Thu Apr 14 16:59:47 2016 +0200
@@ -6,6 +6,7 @@
signature SIMPLIFIER_TRACE =
sig
+ val disable: Proof.context -> Proof.context
val add_term_breakpoint: term -> Context.generic -> Context.generic
val add_thm_breakpoint: thm -> Context.generic -> Context.generic
end
@@ -63,6 +64,13 @@
val get_data = Data.get o Context.Proof
val put_data = Context.proof_map o Data.put
+val disable =
+ Config.put simp_trace false #>
+ (Context.proof_map o Data.map)
+ (fn {max_depth, mode = _, interactive, parent, memory, breakpoints} =>
+ {max_depth = max_depth, mode = Disabled, interactive = interactive, parent = parent,
+ memory = memory, breakpoints = breakpoints});
+
val get_breakpoints = #breakpoints o get_data
fun map_breakpoints f =