# HG changeset patch
# User wenzelm
# Date 1345719809 -7200
# Node ID 44a6967240b77866d20197cddc4aae81a86d7298
# Parent  5e0455e2933907b5cd108ff2bb1537da3450f82f
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

diff -r 5e0455e29339 -r 44a6967240b7 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -84,7 +84,7 @@
       | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
     and strip_spaces_in_list _ [] accum = accum
       | strip_spaces_in_list true (#"%" :: cs) accum =
-        strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd)
+        strip_spaces_in_list true (cs |> take_prefix (not_equal #"\n") |> snd)
                              accum
       | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum =
         strip_c_style_comment cs accum
diff -r 5e0455e29339 -r 44a6967240b7 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -51,7 +51,7 @@
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, ls) = split_first (snd (chop_while empty_line lines))
+    val (l, ls) = split_first (snd (take_prefix empty_line lines))
   in (test_outcome solver_name l, ls) end
 
 
diff -r 5e0455e29339 -r 44a6967240b7 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -96,7 +96,7 @@
       SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
     val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
 
-    val ls = rev (snd (chop_while (equal "") (rev res)))
+    val ls = fst (take_suffix (equal "") res)
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
 
     val _ = return_code <> 0 andalso
diff -r 5e0455e29339 -r 44a6967240b7 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -2772,7 +2772,7 @@
               (* go back up the stack until we find a level where we can go *)
               (* to the next sibling node                                   *)
               let
-                val offsets' = snd (chop_while
+                val offsets' = snd (take_prefix
                   (fn off' => off' mod size_elem = size_elem - 1) offsets)
               in
                 case offsets' of
diff -r 5e0455e29339 -r 44a6967240b7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/Pure/Isar/code.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -1017,7 +1017,7 @@
     val c = const_eqn thy thm;
     fun update_subsume thy (thm, proper) eqns = 
       let
-        val args_of = snd o chop_while is_Var o rev o snd o strip_comb
+        val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
           o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
         val args = args_of thm;
         val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
diff -r 5e0455e29339 -r 44a6967240b7 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/Pure/library.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -74,7 +74,6 @@
   val take: int -> 'a list -> 'a list
   val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
-  val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
   val chop_groups: int -> 'a list -> 'a list list
   val nth: 'a list -> int -> 'a
   val nth_list: 'a list list -> int -> 'a list
@@ -413,10 +412,6 @@
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-fun chop_while P [] = ([], [])
-  | chop_while P (ys as x :: xs) =
-      if P x then chop_while P xs |>> cons x else ([], ys);
-
 fun chop_groups n list =
   (case chop (Int.max (n, 1)) list of
     ([], _) => []
diff -r 5e0455e29339 -r 44a6967240b7 src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/Tools/case_product.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -48,8 +48,8 @@
     val concl = Thm.concl_of thm1
 
     fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
-    val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1)
-    val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2)
+    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
+    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
 
     val p_cases_prod = map (fn p1 => map (fn p2 =>
       let