--- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
@@ -45,8 +45,7 @@
|> #1
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
+ facts = facts |> map Untranslated_Fact}
in
(case prover params (K (K (K ""))) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME