# HG changeset patch
# User wenzelm
# Date 1460645987 -7200
# Node ID ba9072b303a21fb1ec3ce2159f7e9df8cf1ab121
# Parent  4b71cd0bfe142423d7eaabeb674ff697c5cdf9a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;

diff -r 4b71cd0bfe14 -r ba9072b303a2 src/Pure/Tools/simplifier_trace.ML
--- 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 =
diff -r 4b71cd0bfe14 -r ba9072b303a2 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Apr 14 16:02:22 2016 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 14 16:59:47 2016 +0200
@@ -293,17 +293,19 @@
   if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
   then writeln s else ();
 
-fun test_terms ctxt (limit_time, is_interactive) insts goals =
-  (case active_testers ctxt of
-    [] => error "No active testers for quickcheck"
-  | testers =>
-      limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
-        (fn () =>
-          Par_List.get_some (fn tester =>
-            tester ctxt (length testers > 1) insts goals |>
-            (fn result => if exists found_counterexample result then SOME result else NONE))
-          testers)
-        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
+fun test_terms ctxt0 (limit_time, is_interactive) insts goals =
+  let val ctxt = Simplifier_Trace.disable ctxt0 in
+    (case active_testers ctxt of
+      [] => error "No active testers for quickcheck"
+    | testers =>
+        limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+          (fn () =>
+            Par_List.get_some (fn tester =>
+              tester ctxt (length testers > 1) insts goals |>
+              (fn result => if exists found_counterexample result then SOME result else NONE))
+            testers)
+          (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ())
+  end
 
 fun all_axioms_of ctxt t =
   let