--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 10:21:52 2010 +0200
@@ -60,7 +60,7 @@
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, goal, ...} = Proof.goal state
val problem =
- {ctxt = ctxt, goal = goal, subgoal = subgoal,
+ {state = state, goal = goal, subgoal = subgoal,
axioms = map (prepare_axiom ctxt) axioms}
val result as {outcome, used_thm_names, ...} = prover params (K "") problem
in