changeset 45520 | 2b1dde0b1c30 |
parent 45519 | cd6e78cb6ee8 |
child 45574 | 7a39df11bcf6 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 16:35:19 2011 +0100 @@ -71,7 +71,7 @@ {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} val result as {outcome, used_facts, run_time, ...} = - prover params (K (K "")) problem + prover params (K (K (K ""))) problem in print silent (fn () =>