src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 23:10:01 2010 +0200
@@ -321,8 +321,7 @@
           relevance_override chained_ths hyp_ts concl_t
     val problem =
       {ctxt = ctxt', goal = goal, subgoal = i,
-       axiom_ts = map (prop_of o snd) axioms,
-       prepared_axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
+       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
     val time_limit =
       (case hard_timeout of
         NONE => I