tuned;
authorwenzelm
Sun Sep 21 19:53:50 2014 +0200 (2014-09-21)
changeset 58411e3d0354d2129
parent 58410 6d46ad54a2ab
child 58412 f65f11f4854c
tuned;
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/Tools/ATP/atp_waldmeister.ML
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Sep 21 16:56:11 2014 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Sep 21 19:53:50 2014 +0200
     1.3 @@ -914,7 +914,7 @@
     1.4                          (*point to the split node, so that custom rule can be built later on*)
     1.5                          Step n :: (Split (split_node, n, parents)) :: (*this will create the elimination rule*)
     1.6                           naive_skeleton' stop_just_befores split_node @ (*this will discharge the major premise*)
     1.7 -                         List.concat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
     1.8 +                         flat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
     1.9                        end
    1.10                      else if length parents > 1 then
    1.11                        (*Handle fan-in nodes which aren't split-sinks by
    1.12 @@ -1729,9 +1729,9 @@
    1.13            paths'
    1.14            |> ListPair.unzip (*we get a list of pairs of lists. we want a pair of lists*)
    1.15            |> (fn (paths, branch_ids) =>
    1.16 -               (List.concat paths,
    1.17 +               (flat paths,
    1.18                  (*remove duplicate branch_ids*)
    1.19 -                fold (Library.insert (op =)) (List.concat branch_ids) []))
    1.20 +                fold (Library.insert (op =)) (flat branch_ids) []))
    1.21            (*filter paths having branch_ids appearing in the second list*)
    1.22            |> (fn (paths, branch_ids) =>
    1.23                filter (fn (info, _) =>
     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Sun Sep 21 16:56:11 2014 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Sun Sep 21 19:53:50 2014 +0200
     2.3 @@ -122,8 +122,7 @@
     2.4      fun permute' (l, []) = [(l, [])]
     2.5        | permute' (l, xs) =
     2.6            map (fn x => (x :: l, filter (fn y => y <> x) xs)) xs
     2.7 -          |> map permute'
     2.8 -          |> List.concat
     2.9 +          |> maps permute'
    2.10    in
    2.11      permute' ([], l)
    2.12      |> map fst
     3.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 16:56:11 2014 +0200
     3.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 19:53:50 2014 +0200
     3.3 @@ -798,8 +798,7 @@
     3.4          | _ => acc
     3.5    in
     3.6      map (strip_top_All_vars #> snd) conclusions
     3.7 -    |> map (get_skolem_terms [] [])
     3.8 -    |> List.concat
     3.9 +    |> maps (get_skolem_terms [] [])
    3.10      |> distinct (op =)
    3.11    end
    3.12  *}
    3.13 @@ -935,8 +934,7 @@
    3.14                 Logic.strip_horn #> snd #>
    3.15                 get_skolem_conc)
    3.16            |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
    3.17 -          |> map (switch Term.add_vars [])
    3.18 -          |> List.concat
    3.19 +          |> maps (switch Term.add_vars [])
    3.20  
    3.21          fun make_var pre_var =
    3.22            the_single pre_var
    3.23 @@ -1412,7 +1410,7 @@
    3.24        if List.all is_none opt_list then false
    3.25        else
    3.26          fold_options opt_list
    3.27 -        |> List.concat
    3.28 +        |> flat
    3.29          |> pair sought_sublist
    3.30          |> subset (op =)
    3.31    in
    3.32 @@ -2101,11 +2099,10 @@
    3.33      fun get_binds source_inf_opt =
    3.34        case the source_inf_opt of
    3.35            TPTP_Proof.Inference (_, _, parent_inf) =>
    3.36 -            List.map
    3.37 +            maps
    3.38                (fn TPTP_Proof.Parent _ => []
    3.39                  | TPTP_Proof.ParentWithDetails (_, parent_details) => parent_details)
    3.40                parent_inf
    3.41 -            |> List.concat
    3.42          | _ => []
    3.43  
    3.44      val inference_name =
     4.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 16:56:11 2014 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 19:53:50 2014 +0200
     4.3 @@ -708,9 +708,8 @@
     4.4        case results of
     4.5            Nonempty (SOME results') =>
     4.6              #2 results'
     4.7 -            |> map (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
     4.8 +            |> maps (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
     4.9                   if inf_name = inference_name then [inf_fmla] else [])
    4.10 -            |> List.concat
    4.11          | _ => []
    4.12    in Specific_rule (filename, inference_name, filtered_results) end
    4.13  
     5.1 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sun Sep 21 16:56:11 2014 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sun Sep 21 19:53:50 2014 +0200
     5.3 @@ -589,5 +589,5 @@
     5.4        end
     5.5    
     5.6  fun introduce_waldmeister_skolems info proof_steps = proof_steps
     5.7 -      |> map (skolemization_steps info) |> List.concat
     5.8 +      |> maps (skolemization_steps info)
     5.9  end;