# HG changeset patch
# User wenzelm
# Date 1411322030 -7200
# Node ID e3d0354d2129bc0d9229e153ebaaf5f48e2f538f
# Parent  6d46ad54a2abeabe0a9d12d4c37004fe65d9bfb8
tuned;

diff -r 6d46ad54a2ab -r e3d0354d2129 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Sep 21 19:53:50 2014 +0200
@@ -914,7 +914,7 @@
                         (*point to the split node, so that custom rule can be built later on*)
                         Step n :: (Split (split_node, n, parents)) :: (*this will create the elimination rule*)
                          naive_skeleton' stop_just_befores split_node @ (*this will discharge the major premise*)
-                         List.concat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
+                         flat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
                       end
                     else if length parents > 1 then
                       (*Handle fan-in nodes which aren't split-sinks by
@@ -1729,9 +1729,9 @@
           paths'
           |> ListPair.unzip (*we get a list of pairs of lists. we want a pair of lists*)
           |> (fn (paths, branch_ids) =>
-               (List.concat paths,
+               (flat paths,
                 (*remove duplicate branch_ids*)
-                fold (Library.insert (op =)) (List.concat branch_ids) []))
+                fold (Library.insert (op =)) (flat branch_ids) []))
           (*filter paths having branch_ids appearing in the second list*)
           |> (fn (paths, branch_ids) =>
               filter (fn (info, _) =>
diff -r 6d46ad54a2ab -r e3d0354d2129 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Sun Sep 21 19:53:50 2014 +0200
@@ -122,8 +122,7 @@
     fun permute' (l, []) = [(l, [])]
       | permute' (l, xs) =
           map (fn x => (x :: l, filter (fn y => y <> x) xs)) xs
-          |> map permute'
-          |> List.concat
+          |> maps permute'
   in
     permute' ([], l)
     |> map fst
diff -r 6d46ad54a2ab -r e3d0354d2129 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 19:53:50 2014 +0200
@@ -798,8 +798,7 @@
         | _ => acc
   in
     map (strip_top_All_vars #> snd) conclusions
-    |> map (get_skolem_terms [] [])
-    |> List.concat
+    |> maps (get_skolem_terms [] [])
     |> distinct (op =)
   end
 *}
@@ -935,8 +934,7 @@
                Logic.strip_horn #> snd #>
                get_skolem_conc)
           |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
-          |> map (switch Term.add_vars [])
-          |> List.concat
+          |> maps (switch Term.add_vars [])
 
         fun make_var pre_var =
           the_single pre_var
@@ -1412,7 +1410,7 @@
       if List.all is_none opt_list then false
       else
         fold_options opt_list
-        |> List.concat
+        |> flat
         |> pair sought_sublist
         |> subset (op =)
   in
@@ -2101,11 +2099,10 @@
     fun get_binds source_inf_opt =
       case the source_inf_opt of
           TPTP_Proof.Inference (_, _, parent_inf) =>
-            List.map
+            maps
               (fn TPTP_Proof.Parent _ => []
                 | TPTP_Proof.ParentWithDetails (_, parent_details) => parent_details)
               parent_inf
-            |> List.concat
         | _ => []
 
     val inference_name =
diff -r 6d46ad54a2ab -r e3d0354d2129 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 19:53:50 2014 +0200
@@ -708,9 +708,8 @@
       case results of
           Nonempty (SOME results') =>
             #2 results'
-            |> map (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
+            |> maps (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
                  if inf_name = inference_name then [inf_fmla] else [])
-            |> List.concat
         | _ => []
   in Specific_rule (filename, inference_name, filtered_results) end
 
diff -r 6d46ad54a2ab -r e3d0354d2129 src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sun Sep 21 19:53:50 2014 +0200
@@ -589,5 +589,5 @@
       end
   
 fun introduce_waldmeister_skolems info proof_steps = proof_steps
-      |> map (skolemization_steps info) |> List.concat
+      |> maps (skolemization_steps info)
 end;