src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 23:10:01 2010 +0200
@@ -60,8 +60,7 @@
     val {context = ctxt, goal, ...} = Proof.goal state
     val problem =
       {ctxt = ctxt, goal = goal, subgoal = subgoal,
-       axiom_ts = map (prop_of o snd) axioms,
-       prepared_axioms = map (prepare_axiom ctxt) axioms}
+       axioms = map (prepare_axiom ctxt) axioms}
     val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
     priority (case outcome of