src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
changeset 42915 889d767ce5f4
parent 42695 1b447261865e
child 43051 a6c141925a8a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Mar 22 12:49:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Mar 22 17:20:53 2011 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4                        (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
     1.5          end
     1.6      val params =
     1.7 -      {debug = debug, verbose = false, overlord = overlord, blocking = true,
     1.8 +      {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
     1.9         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    1.10         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    1.11         isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,