# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID fa0926e40759dfefc867cfd969fe223b1e029f86
# Parent  95bab16eac45216cacfad4a0dba3416551ad7f87
tuned tracing output (indirectly)

diff -r 95bab16eac45 -r fa0926e40759 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -37,12 +37,12 @@
 val slack = seconds 0.025
 
 fun minimized_isar_step ctxt time
-    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
+    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meth :: _, comment)) =
   let
     val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
 
     fun mk_step_lfs_gfs lfs gfs =
-      Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
+      Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), [meth], comment)
 
     fun minimize_half _ min_facts [] time = (min_facts, time)
       | minimize_half mk_step min_facts (fact :: facts) time =