changeset 41741 | 839d1488045f |
parent 41491 | a2ad5b824051 |
child 41742 | 11e862c68b40 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100 @@ -67,7 +67,7 @@ val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, smt_head = NONE} + facts = facts, smt_filter = NONE} val result as {outcome, used_facts, ...} = prover params (K "") problem in print silent (fn () =>