prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
authorwenzelm
Thu Aug 23 13:03:29 2012 +0200 (2012-08-23)
changeset 4890244a6967240b7
parent 48901 5e0455e29339
child 48903 1621b3f26095
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/refute.ML
src/Pure/Isar/code.ML
src/Pure/library.ML
src/Tools/case_product.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 12:55:23 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 13:03:29 2012 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4        | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
     1.5      and strip_spaces_in_list _ [] accum = accum
     1.6        | strip_spaces_in_list true (#"%" :: cs) accum =
     1.7 -        strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd)
     1.8 +        strip_spaces_in_list true (cs |> take_prefix (not_equal #"\n") |> snd)
     1.9                               accum
    1.10        | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum =
    1.11          strip_c_style_comment cs accum
     2.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Aug 23 12:55:23 2012 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Aug 23 13:03:29 2012 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4    let
     2.5      val empty_line = (fn "" => true | _ => false)
     2.6      val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
     2.7 -    val (l, ls) = split_first (snd (chop_while empty_line lines))
     2.8 +    val (l, ls) = split_first (snd (take_prefix empty_line lines))
     2.9    in (test_outcome solver_name l, ls) end
    2.10  
    2.11  
     3.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 23 12:55:23 2012 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 23 13:03:29 2012 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4        SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
     3.5      val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
     3.6  
     3.7 -    val ls = rev (snd (chop_while (equal "") (rev res)))
     3.8 +    val ls = fst (take_suffix (equal "") res)
     3.9      val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
    3.10  
    3.11      val _ = return_code <> 0 andalso
     4.1 --- a/src/HOL/Tools/refute.ML	Thu Aug 23 12:55:23 2012 +0200
     4.2 +++ b/src/HOL/Tools/refute.ML	Thu Aug 23 13:03:29 2012 +0200
     4.3 @@ -2772,7 +2772,7 @@
     4.4                (* go back up the stack until we find a level where we can go *)
     4.5                (* to the next sibling node                                   *)
     4.6                let
     4.7 -                val offsets' = snd (chop_while
     4.8 +                val offsets' = snd (take_prefix
     4.9                    (fn off' => off' mod size_elem = size_elem - 1) offsets)
    4.10                in
    4.11                  case offsets' of
     5.1 --- a/src/Pure/Isar/code.ML	Thu Aug 23 12:55:23 2012 +0200
     5.2 +++ b/src/Pure/Isar/code.ML	Thu Aug 23 13:03:29 2012 +0200
     5.3 @@ -1017,7 +1017,7 @@
     5.4      val c = const_eqn thy thm;
     5.5      fun update_subsume thy (thm, proper) eqns = 
     5.6        let
     5.7 -        val args_of = snd o chop_while is_Var o rev o snd o strip_comb
     5.8 +        val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
     5.9            o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
    5.10          val args = args_of thm;
    5.11          val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     6.1 --- a/src/Pure/library.ML	Thu Aug 23 12:55:23 2012 +0200
     6.2 +++ b/src/Pure/library.ML	Thu Aug 23 13:03:29 2012 +0200
     6.3 @@ -74,7 +74,6 @@
     6.4    val take: int -> 'a list -> 'a list
     6.5    val drop: int -> 'a list -> 'a list
     6.6    val chop: int -> 'a list -> 'a list * 'a list
     6.7 -  val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
     6.8    val chop_groups: int -> 'a list -> 'a list list
     6.9    val nth: 'a list -> int -> 'a
    6.10    val nth_list: 'a list list -> int -> 'a list
    6.11 @@ -413,10 +412,6 @@
    6.12    | chop _ [] = ([], [])
    6.13    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    6.14  
    6.15 -fun chop_while P [] = ([], [])
    6.16 -  | chop_while P (ys as x :: xs) =
    6.17 -      if P x then chop_while P xs |>> cons x else ([], ys);
    6.18 -
    6.19  fun chop_groups n list =
    6.20    (case chop (Int.max (n, 1)) list of
    6.21      ([], _) => []
     7.1 --- a/src/Tools/case_product.ML	Thu Aug 23 12:55:23 2012 +0200
     7.2 +++ b/src/Tools/case_product.ML	Thu Aug 23 13:03:29 2012 +0200
     7.3 @@ -48,8 +48,8 @@
     7.4      val concl = Thm.concl_of thm1
     7.5  
     7.6      fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
     7.7 -    val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1)
     7.8 -    val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2)
     7.9 +    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
    7.10 +    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
    7.11  
    7.12      val p_cases_prod = map (fn p1 => map (fn p2 =>
    7.13        let