chop_while replace drop_while and take_while

--- a/src/HOL/Tools/SMT/cvc3_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/cvc3_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -27,7 +27,7 @@
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, _) = split_first (drop_while empty_line output)
+    val (l, _) = split_first (snd (chop_while empty_line output))
   in
     if is_unsat l then @{cprop False}
     else if is_sat l then raise_cex true

--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -160,7 +160,7 @@
     val (res, err) = with_timeout ctxt (run ctxt cmd args) input
     val _ = trace_msg ctxt (pretty "SMT solver:") err
 
-    val ls = rev (drop_while (equal "") (rev res))
+    val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in ls end
 

--- a/src/HOL/Tools/SMT/yices_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/yices_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -23,7 +23,7 @@
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, _) = split_first (drop_while empty_line output)
+    val (l, _) = split_first (snd (chop_while empty_line output))
   in
     if String.isPrefix "unsat" l then @{cprop False}
     else if String.isPrefix "sat" l then raise_cex true

--- a/src/HOL/Tools/refute.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -2772,8 +2772,8 @@
               (* go back up the stack until we find a level where we can go *)
               (* to the next sibling node                                   *)
               let
-                val offsets' = drop_while
-                  (fn off' => off' mod size_elem = size_elem - 1) offsets
+                val offsets' = snd (chop_while
+                  (fn off' => off' mod size_elem = size_elem - 1) offsets)
               in
                 case offsets' of
                   [] =>

--- a/src/Pure/Isar/code.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/Pure/Isar/code.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -1049,7 +1049,7 @@
     val c = const_eqn thy thm;
     fun update_subsume thy (thm, proper) eqns = 
       let
-        val args_of = drop_while is_Var o rev o snd o strip_comb
+        val args_of = snd o chop_while 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);

--- a/src/Pure/library.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/Pure/library.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -83,8 +83,7 @@
   val take: int -> 'a list -> 'a list
   val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
-  val take_while: ('a -> bool) -> 'a list -> 'a list
-  val drop_while: ('a -> bool) -> 'a list -> 'a list
+  val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
   val nth: 'a list -> int -> 'a
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val nth_drop: int -> 'a list -> 'a list
@@ -422,11 +421,9 @@
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-fun drop_while P [] = []
-  | drop_while P (ys as x :: xs) = if P x then drop_while P xs else ys;
-
-fun take_while P [] = []
-  | take_while P (x :: xs) = if P x then x :: take_while P xs else [];
+fun chop_while P [] = ([], [])
+  | chop_while P (ys as x :: xs) =
+      if P x then chop_while P xs |>> cons x else ([], ys);
 
 (*return nth element of a list, where 0 designates the first element;
   raise Subscript if list too short*)