# HG changeset patch
# User wenzelm
# Date 1517164132 -3600
# Node ID 9e712280cc372088fea92157c51f3adeb8a61660
# Parent  6a27e86cc2e7a4d2ec78a6a0bc112bc887de2196
clarified take/drop/chop prefix/suffix;

diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -73,7 +73,7 @@
     (case t of
       Var (xi, _) =>
         let
-          val (bounds, tail) = take_prefix is_Bound ts;
+          val (bounds, tail) = chop_prefix is_Bound ts;
         in
           list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
         end
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Library/refute.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -1943,7 +1943,7 @@
                         else ()
                       (* split the constructors into those occurring before/after *)
                       (* 'Const (s, T)'                                          *)
-                      val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
+                      val (constrs1, constrs2) = chop_prefix (fn (cname, ctypes) =>
                         not (cname = s andalso Sign.typ_instance thy (T,
                           map (typ_of_dtyp descr typ_assoc) ctypes
                             ---> Type (s', Ts')))) constrs
@@ -2656,8 +2656,7 @@
               (* go back up the stack until we find a level where we can go *)
               (* to the next sibling node                                   *)
               let
-                val offsets' = snd (take_prefix
-                  (fn off' => off' mod size_elem = size_elem - 1) offsets)
+                val offsets' = drop_prefix (fn off' => off' mod size_elem = size_elem - 1) offsets
               in
                 case offsets' of
                   [] =>
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -330,7 +330,7 @@
              rotate_tac 1 1,
              REPEAT (eresolve_tac ctxt' [conjE] 1)])
           [] ctxt;
-        val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets);
+        val (Ts1, _ :: Ts2) = chop_prefix (not o equal T) (map snd sets);
         val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2);
         val (pis1, pis2) = chop (length Ts1)
           (map Bound (length pTs - 1 downto 0));
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -50,8 +50,8 @@
           else raise RecError "illegal head of function equation"
       | _ => raise RecError "illegal head of function equation";
 
-    val (ls', rest)  = take_prefix is_Free args;
-    val (middle, rs') = take_suffix is_Free rest;
+    val (ls', rest)  = chop_prefix is_Free args;
+    val (middle, rs') = chop_suffix is_Free rest;
     val rpos = length ls';
 
     val (constr, cargs') = if null middle then raise RecError "constructor missing"
@@ -296,7 +296,7 @@
     val rec_rewritess =
       unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites;
     val fvars = rec_rewrites |> hd |> Thm.concl_of |> HOLogic.dest_Trueprop |>
-      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
+      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var;
     val (pvars, ctxtvars) = List.partition
       (equal HOLogic.boolT o body_type o snd)
       (subtract (op =)
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -180,7 +180,7 @@
 
 fun beginning n cs =
   let
-    val drop_blanks = #1 o take_suffix is_whitespace;
+    val drop_blanks = drop_suffix is_whitespace;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -33,7 +33,7 @@
 
 fun err_unfinished () = error "An unfinished SPARK environment is still open."
 
-val strip_number = apply2 implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
+val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
 
 val name_ord = prod_ord string_ord (option_ord int_ord) o
   apply2 (strip_number ##> Int.fromString);
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -696,7 +696,7 @@
         (case strip_comb t of
           (Free (s, _), args as _ :: _) =>
           if String.isPrefix spass_skolem_prefix s then
-            insert (op =) (s, fst (take_prefix is_Var args))
+            insert (op =) (s, take_prefix is_Var args)
           else
             fold add_skolem_args args
         | (u, args as _ :: _) => fold add_skolem_args (u :: args)
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -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 |> take_prefix (not_equal #"\n") |> snd) accum
+        strip_spaces_in_list true (cs |> drop_prefix (not_equal #"\n")) accum
       | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = strip_c_style_comment cs accum
       | strip_spaces_in_list _ [c1] accum = accum |> not (is_spaceish c1) ? cons c1
       | strip_spaces_in_list skip_comments (cs as [_, _]) accum =
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -296,8 +296,8 @@
       handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn];
     val (fun_name, args) = strip_comb lhs
       |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]);
-    val (left_args, rest) = take_prefix is_Free args;
-    val (nonfrees, right_args) = take_suffix is_Free rest;
+    val (left_args, rest) = chop_prefix is_Free args;
+    val (nonfrees, right_args) = chop_suffix is_Free rest;
     val num_nonfrees = length nonfrees;
     val _ = num_nonfrees = 1 orelse
       (if num_nonfrees = 0 then missing_pattern ctxt [eqn]
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -75,7 +75,7 @@
           val _ $ Pxs = Logic.strip_assums_concl conc
           val (P, _) = strip_comb Pxs
           val (cases', conds) =
-            take_prefix (Term.exists_subterm (curry op aconv P)) cases
+            chop_prefix (Term.exists_subterm (curry op aconv P)) cases
           val concl' = fold_rev (curry Logic.mk_implies) conds conc
         in
           ([mk_branch concl'], cases')
@@ -101,7 +101,7 @@
         fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
 
         val (gs, rcprs) =
-          take_prefix (not o Term.exists_subterm is_pred) prems
+          chop_prefix (not o Term.exists_subterm is_pred) prems
       in
         SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
           gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -730,7 +730,7 @@
 (*This version does only one inference per call;
   having only one eq_assume_tac speeds it up!*)
 fun prolog_step_tac' ctxt horns =
-    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
+    let val horn0s = (*0 subgoals vs 1 or more*)
             take_prefix Thm.no_prems horns
         val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
     in  fn i => eq_assume_tac i ORELSE
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -49,8 +49,8 @@
           else primrec_error "illegal head of function equation"
       | _ => primrec_error "illegal head of function equation");
 
-    val (ls', rest)  = take_prefix is_Free args;
-    val (middle, rs') = take_suffix is_Free rest;
+    val (ls', rest)  = chop_prefix is_Free args;
+    val (middle, rs') = chop_suffix is_Free rest;
     val rpos = length ls';
 
     val (constr, cargs') =
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -202,7 +202,7 @@
                       (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
                     Quickcheck.message ctxt
                       "Quickcheck continues to find a genuine counterexample...";
-                    test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
+                    test true (drop_prefix (fn x => not (x = (card, size))) enum)
                 end
             | NONE => ())
         in (test genuine_only enumeration_card_size; !current_result) end)
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -94,7 +94,7 @@
       SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
     val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
 
-    val output = fst (take_suffix (equal "") res)
+    val output = drop_suffix (equal "") res
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
 
     val _ = member (op =) normal_return_codes return_code orelse
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -33,7 +33,7 @@
 fun on_first_line test_outcome solver_name lines =
   let
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
+    val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
   in (test_outcome solver_name l, ls) end
 
 fun on_first_non_unsupported_line test_outcome solver_name lines =
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/SMT/smtlib.ML
--- a/src/HOL/Tools/SMT/smtlib.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smtlib.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -40,7 +40,7 @@
 (* utilities *)
 
 fun read_raw pred l cs =
-  (case take_prefix pred cs of
+  (case chop_prefix pred cs of
     ([], []) => raise PARSE (l, "empty token")
   | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
   | x => x)
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -362,7 +362,7 @@
         Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
     val (perfect, imperfect) = candidates
       |> sort (Real.compare o swap o apply2 snd)
-      |> take_prefix (fn (_, w) => w > 0.99999)
+      |> chop_prefix (fn (_, w) => w > 0.99999)
     val ((accepts, more_rejects), rejects) =
       chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   in
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -307,7 +307,7 @@
       | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
     fun clauses xs =
       let
-        val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
+        val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs
       in
         case xs2 of
           []      => [xs1]
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -49,7 +49,7 @@
     fun add a (line, lines) = (a :: line, lines);
     fun flush (line, lines) = ([], rev line :: lines);
     fun split (a as Text ss) =
-          (case take_prefix (fn ("\n", _) => false | _ => true) ss of
+          (case chop_prefix (fn ("\n", _) => false | _ => true) ss of
             ([], []) => I
           | (_, []) => add a
           | ([], _ :: rest) => flush #> split (Text rest)
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/path.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -150,7 +150,7 @@
       handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
 
     val (roots, raw_elems) =
-      (case take_prefix (equal "") (space_explode "/" str) |>> length of
+      (case chop_prefix (equal "") (space_explode "/" str) |>> length of
         (0, es) => ([], es)
       | (1, es) => ([Root ""], es)
       | (_, []) => ([Root ""], [])
@@ -190,7 +190,7 @@
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
-  (case take_suffix (fn c => c <> ".") (raw_explode s) of
+  (case chop_suffix (fn c => c <> ".") (raw_explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/pretty.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -128,7 +128,7 @@
     val indent' = force_nat indent;
     fun body_length prts len =
       let
-        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
+        val (line, rest) = chop_prefix (fn Break (true, _, _) => false | _ => true) prts;
         val len' = Int.max (fold (Integer.add o length) line 0, len);
       in
         (case rest of
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/symbol.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -199,7 +199,7 @@
 
 fun beginning n cs =
   let
-    val drop_blanks = #1 o take_suffix is_ascii_blank;
+    val drop_blanks = drop_suffix is_ascii_blank;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
@@ -465,7 +465,7 @@
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
-    val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
+    val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;
 
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/code.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -1380,7 +1380,7 @@
 
 fun subsumptive_add thy verbose (thm, proper) eqns =
   let
-    val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
+    val args_of = drop_prefix is_Var o rev o snd o strip_comb
       o Term.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 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/element.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -233,7 +233,7 @@
     val concl_term = Object_Logic.drop_judgment ctxt concl;
 
     val (assumes, cases) =
-      take_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
+      chop_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
     val is_thesis = if null cases then K false else fn v => v aconv concl_term;
     val fixes =
       rev (fold_aterms (fn v as Free (x, T) =>
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -975,7 +975,7 @@
 
 fun implicit_vars props =
   let
-    val (var_props, _) = take_prefix is_var props;
+    val var_props = take_prefix is_var props;
     val explicit_vars = fold Term.add_vars var_props [];
     val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
   in map (Logic.mk_term o Var) vars end;
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -1536,7 +1536,7 @@
     val print_name = Token.print_name (Thy_Header.get_keywords' ctxt);
 
     fun trim_name x = if Name.is_internal x then Name.clean x else "_";
-    val trim_names = map trim_name #> take_suffix (equal "_") #> #1;
+    val trim_names = map trim_name #> drop_suffix (equal "_");
 
     fun print_case name xs =
       (case trim_names xs of
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -131,7 +131,7 @@
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
-    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
+    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -70,7 +70,7 @@
   | rlz_proc _ = NONE;
 
 val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
-  take_prefix (fn s => s <> ":") o raw_explode;
+  chop_prefix (fn s => s <> ":") o raw_explode;
 
 type rules =
   {next: int, rs: ((term * term) list * (term * term)) list,
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -406,7 +406,7 @@
   let
     val cs = Symbol.explode str;
     val (intpart, fracpart) =
-      (case take_prefix Symbol.is_digit cs of
+      (case chop_prefix Symbol.is_digit cs of
         (intpart, "." :: fracpart) => (intpart, fracpart)
       | _ => raise Fail "read_float");
   in
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Thy/markdown.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -90,7 +90,7 @@
 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
 
 fun strip_spaces (Antiquote.Text ss :: rest) =
-      let val (sp, ss') = take_prefix is_space ss
+      let val (sp, ss') = chop_prefix is_space ss
       in (length sp, if null ss' then rest else Antiquote.Text ss' :: rest) end
   | strip_spaces source = (0, source);
 
@@ -149,7 +149,7 @@
 
 fun list_items [] = []
   | list_items (item :: rest) =
-      let val (item_rest, rest') = take_prefix (not o is_item) rest;
+      let val (item_rest, rest') = chop_prefix (not o is_item) rest;
       in (item :: item_rest) :: list_items rest' end;
 
 
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -209,16 +209,16 @@
 
 fun make_span cmd src =
   let
-    fun take_newline (tok :: toks) =
+    fun chop_newline (tok :: toks) =
           if newline_token (fst tok) then ([tok], toks, true)
           else ([], tok :: toks, false)
-      | take_newline [] = ([], [], false);
+      | chop_newline [] = ([], [], false);
     val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
       src
-      |> take_prefix (white_token o fst)
-      ||>> take_suffix (white_token o fst)
-      ||>> take_prefix (white_comment_token o fst)
-      ||> take_newline;
+      |> chop_prefix (white_token o fst)
+      ||>> chop_suffix (white_token o fst)
+      ||>> chop_prefix (white_comment_token o fst)
+      ||> chop_newline;
   in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
 
 
@@ -405,7 +405,7 @@
           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = toks
-      |> take_suffix Token.is_space |> #1
+      |> drop_suffix Token.is_space
       |> Source.of_list
       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
       |> Source.source stopper (Scan.error (Scan.bulk span))
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/library.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -99,9 +99,13 @@
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
+  val take_prefix: ('a -> bool) -> 'a list -> 'a list
+  val drop_prefix: ('a -> bool) -> 'a list -> 'a list
+  val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val take_suffix: ('a -> bool) -> 'a list -> 'a list
+  val drop_suffix: ('a -> bool) -> 'a list -> 'a list
+  val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
-  val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   val prefixes1: 'a list -> 'a list list
   val prefixes: 'a list -> 'a list list
@@ -526,28 +530,53 @@
 fun burrow_fst f xs = split_list xs |>> f |> op ~~;
 
 
+(* take, drop, chop, trim according to predicate *)
+
+fun take_prefix pred list =
+  let
+    fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res
+      | take res [] = rev res;
+  in take [] list end;
+
+fun drop_prefix pred list =
+  let
+    fun drop (x :: xs) = if pred x then drop xs else x :: xs
+      | drop [] = [];
+  in drop list end;
+
+fun chop_prefix pred list =
+  let
+    val prfx = take_prefix pred list;
+    val sffx = drop (length prfx) list;
+  in (prfx, sffx) end;
+
+fun take_suffix pred list =
+  let
+    fun take res (x :: xs) = if pred x then take (x :: res) xs else res
+      | take res [] = res;
+  in take [] (rev list) end;
+
+fun drop_suffix pred list =
+  let
+    fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs)
+      | drop [] = [];
+  in drop (rev list) end;
+
+fun chop_suffix pred list =
+  let
+    val prfx = drop_suffix pred list;
+    val sffx = drop (length prfx) list;
+  in (prfx, sffx) end;
+
+fun trim pred = drop_prefix pred #> drop_suffix pred;
+
+
 (* prefixes, suffixes *)
 
 fun is_prefix _ [] _ = true
   | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys
   | is_prefix eq _ _ = false;
 
-(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., x(i-1)], [xi, ..., xn])
-   where xi is the first element that does not satisfy the predicate*)
-fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
-  let fun take (rxs, []) = (rev rxs, [])
-        | take (rxs, x :: xs) =
-            if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
-  in  take([], xs)  end;
-
-(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
-   where xi is the last element that does not satisfy the predicate*)
-fun take_suffix _ [] = ([], [])
-  | take_suffix pred (x :: xs) =
-      (case take_suffix pred xs of
-        ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
-      | (prfx, sffx) => (x :: prfx, sffx));
-
 fun chop_common_prefix eq ([], ys) = ([], ([], ys))
   | chop_common_prefix eq (xs, []) = ([], (xs, []))
   | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
@@ -564,8 +593,6 @@
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
 
-fun trim pred = take_prefix pred #> #2 #> take_suffix pred #> #1;
-
 
 (** integers **)
 
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Tools/case_product.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -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) = take_prefix is_consumes (Thm.prems_of thm1)
-    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
+    val (p_cons1, p_cases1) = chop_prefix is_consumes (Thm.prems_of thm1)
+    val (p_cons2, p_cases2) = chop_prefix is_consumes (Thm.prems_of thm2)
 
     val p_cases_prod = map (fn p1 => map (fn p2 =>
       let
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Tools/coherent.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -54,8 +54,7 @@
   let
     val prems = Logic.strip_imp_prems prop;
     val concl = Logic.strip_imp_concl prop;
-    val (prems1, prems2) =
-      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
+    val (prems1, prems2) = chop_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
   in
     (prems1,
      if null prems2 then [([], [concl])]
diff -r 6a27e86cc2e7 -r 9e712280cc37 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -40,8 +40,8 @@
     val (fname, ftype) = dest_Const recfun handle TERM _ =>
       raise RecError "function is not declared as constant in theory";
 
-    val (ls_frees, rest)  = take_prefix is_Free args;
-    val (middle, rs_frees) = take_suffix is_Free rest;
+    val (ls_frees, rest)  = chop_prefix is_Free args;
+    val (middle, rs_frees) = chop_suffix is_Free rest;
 
     val (constr, cargs_frees) =
       if null middle then raise RecError "constructor missing"