# HG changeset patch
# User blanchet
# Date 1403617760 -7200
# Node ID 7938a6881b26dab73e9315840c51b275cbc8c794
# Parent  ff10067b224850c2f165c2adafe3d57fd010a55d
tuning

diff -r ff10067b2248 -r 7938a6881b26 src/HOL/TPTP/atp_theory_export.ML
--- 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
diff -r ff10067b2248 -r 7938a6881b26 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Jun 24 15:08:19 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Jun 24 15:49:20 2014 +0200
@@ -1223,8 +1223,7 @@
         val prems = map4 mk_prem phis ctors FTs_setss xFs;
 
         fun mk_concl phi z = phi $ z;
-        val concl =
-          HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
+        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
 
         val goal = Logic.list_implies (prems, concl);
       in