--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 24 15:08:19 2014 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 24 15:49:20 2014 +0200
@@ -187,8 +187,7 @@
th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
|> these |> map fact_name_of))
val all_problem_names =
- problem |> maps (map ident_of_problem_line o snd)
- |> distinct (op =)
+ problem |> maps (map ident_of_problem_line o snd) |> distinct (op =)
val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
val infers =
infers |> filter (Symtab.defined all_problem_name_set o fst)
@@ -197,16 +196,13 @@
val ordered_names =
String_Graph.empty
|> fold (String_Graph.new_node o rpair ()) all_problem_names
- |> fold (fn (to, froms) =>
- fold (fn from => maybe_add_edge (from, to)) froms)
- infers
+ |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers
|> fold (fn (to, from) => maybe_add_edge (from, to))
- (tl all_problem_names ~~ fst (split_last all_problem_names))
+ (tl all_problem_names ~~ fst (split_last all_problem_names))
|> String_Graph.topological_order
val order_tab =
Symtab.empty
- |> fold (Symtab.insert (op =))
- (ordered_names ~~ (1 upto length ordered_names))
+ |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
in
problem