--- a/src/HOL/TPTP/atp_theory_export.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Dec 12 02:47:45 2012 +0100
@@ -136,13 +136,13 @@
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
- val ths = facts |> map snd
- val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make
+ val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts
val infers =
- facts |> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
- th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
- |> map fact_name_of))
+ facts
+ |> map (fn (_, th) =>
+ (fact_name_of (Thm.get_name_hint th),
+ th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
+ |> map fact_name_of))
val all_atp_problem_names =
atp_problem |> maps (map ident_of_problem_line o snd)
val infers =