clarified take/drop/chop prefix/suffix;
authorwenzelm
Sun Jan 28 19:28:52 2018 +0100 (20 months ago)
changeset 675229e712280cc37
parent 67521 6a27e86cc2e7
child 67523 ed9bc7c2d8de
clarified take/drop/chop prefix/suffix;
src/HOL/Library/conditional_parametricity.ML
src/HOL/Library/refute.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/SPARK/Tools/fdl_lexer.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Old_Datatype/old_primrec.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/smtlib.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/sat_solver.ML
src/Pure/General/antiquote.ML
src/Pure/General/path.ML
src/Pure/General/pretty.ML
src/Pure/General/symbol.ML
src/Pure/Isar/code.ML
src/Pure/Isar/element.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/PIDE/command.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
src/Pure/library.ML
src/Tools/case_product.ML
src/Tools/coherent.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Library/conditional_parametricity.ML	Sun Jan 28 16:09:00 2018 +0100
     1.2 +++ b/src/HOL/Library/conditional_parametricity.ML	Sun Jan 28 19:28:52 2018 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4      (case t of
     1.5        Var (xi, _) =>
     1.6          let
     1.7 -          val (bounds, tail) = take_prefix is_Bound ts;
     1.8 +          val (bounds, tail) = chop_prefix is_Bound ts;
     1.9          in
    1.10            list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
    1.11          end
     2.1 --- a/src/HOL/Library/refute.ML	Sun Jan 28 16:09:00 2018 +0100
     2.2 +++ b/src/HOL/Library/refute.ML	Sun Jan 28 19:28:52 2018 +0100
     2.3 @@ -1943,7 +1943,7 @@
     2.4                          else ()
     2.5                        (* split the constructors into those occurring before/after *)
     2.6                        (* 'Const (s, T)'                                          *)
     2.7 -                      val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
     2.8 +                      val (constrs1, constrs2) = chop_prefix (fn (cname, ctypes) =>
     2.9                          not (cname = s andalso Sign.typ_instance thy (T,
    2.10                            map (typ_of_dtyp descr typ_assoc) ctypes
    2.11                              ---> Type (s', Ts')))) constrs
    2.12 @@ -2656,8 +2656,7 @@
    2.13                (* go back up the stack until we find a level where we can go *)
    2.14                (* to the next sibling node                                   *)
    2.15                let
    2.16 -                val offsets' = snd (take_prefix
    2.17 -                  (fn off' => off' mod size_elem = size_elem - 1) offsets)
    2.18 +                val offsets' = drop_prefix (fn off' => off' mod size_elem = size_elem - 1) offsets
    2.19                in
    2.20                  case offsets' of
    2.21                    [] =>
     3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jan 28 16:09:00 2018 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jan 28 19:28:52 2018 +0100
     3.3 @@ -330,7 +330,7 @@
     3.4               rotate_tac 1 1,
     3.5               REPEAT (eresolve_tac ctxt' [conjE] 1)])
     3.6            [] ctxt;
     3.7 -        val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets);
     3.8 +        val (Ts1, _ :: Ts2) = chop_prefix (not o equal T) (map snd sets);
     3.9          val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2);
    3.10          val (pis1, pis2) = chop (length Ts1)
    3.11            (map Bound (length pTs - 1 downto 0));
     4.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Jan 28 16:09:00 2018 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Jan 28 19:28:52 2018 +0100
     4.3 @@ -50,8 +50,8 @@
     4.4            else raise RecError "illegal head of function equation"
     4.5        | _ => raise RecError "illegal head of function equation";
     4.6  
     4.7 -    val (ls', rest)  = take_prefix is_Free args;
     4.8 -    val (middle, rs') = take_suffix is_Free rest;
     4.9 +    val (ls', rest)  = chop_prefix is_Free args;
    4.10 +    val (middle, rs') = chop_suffix is_Free rest;
    4.11      val rpos = length ls';
    4.12  
    4.13      val (constr, cargs') = if null middle then raise RecError "constructor missing"
    4.14 @@ -296,7 +296,7 @@
    4.15      val rec_rewritess =
    4.16        unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites;
    4.17      val fvars = rec_rewrites |> hd |> Thm.concl_of |> HOLogic.dest_Trueprop |>
    4.18 -      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
    4.19 +      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var;
    4.20      val (pvars, ctxtvars) = List.partition
    4.21        (equal HOLogic.boolT o body_type o snd)
    4.22        (subtract (op =)
     5.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Jan 28 16:09:00 2018 +0100
     5.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Jan 28 19:28:52 2018 +0100
     5.3 @@ -180,7 +180,7 @@
     5.4  
     5.5  fun beginning n cs =
     5.6    let
     5.7 -    val drop_blanks = #1 o take_suffix is_whitespace;
     5.8 +    val drop_blanks = drop_suffix is_whitespace;
     5.9      val all_cs = drop_blanks cs;
    5.10      val dots = if length all_cs > n then " ..." else "";
    5.11    in
     6.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Jan 28 16:09:00 2018 +0100
     6.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Jan 28 19:28:52 2018 +0100
     6.3 @@ -33,7 +33,7 @@
     6.4  
     6.5  fun err_unfinished () = error "An unfinished SPARK environment is still open."
     6.6  
     6.7 -val strip_number = apply2 implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
     6.8 +val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
     6.9  
    6.10  val name_ord = prod_ord string_ord (option_ord int_ord) o
    6.11    apply2 (strip_number ##> Int.fromString);
     7.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Jan 28 16:09:00 2018 +0100
     7.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Jan 28 19:28:52 2018 +0100
     7.3 @@ -696,7 +696,7 @@
     7.4          (case strip_comb t of
     7.5            (Free (s, _), args as _ :: _) =>
     7.6            if String.isPrefix spass_skolem_prefix s then
     7.7 -            insert (op =) (s, fst (take_prefix is_Var args))
     7.8 +            insert (op =) (s, take_prefix is_Var args)
     7.9            else
    7.10              fold add_skolem_args args
    7.11          | (u, args as _ :: _) => fold add_skolem_args (u :: args)
     8.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jan 28 16:09:00 2018 +0100
     8.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jan 28 19:28:52 2018 +0100
     8.3 @@ -84,7 +84,7 @@
     8.4        | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
     8.5      and strip_spaces_in_list _ [] accum = accum
     8.6        | strip_spaces_in_list true (#"%" :: cs) accum =
     8.7 -        strip_spaces_in_list true (cs |> take_prefix (not_equal #"\n") |> snd) accum
     8.8 +        strip_spaces_in_list true (cs |> drop_prefix (not_equal #"\n")) accum
     8.9        | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = strip_c_style_comment cs accum
    8.10        | strip_spaces_in_list _ [c1] accum = accum |> not (is_spaceish c1) ? cons c1
    8.11        | strip_spaces_in_list skip_comments (cs as [_, _]) accum =
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 28 16:09:00 2018 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 28 19:28:52 2018 +0100
     9.3 @@ -296,8 +296,8 @@
     9.4        handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn];
     9.5      val (fun_name, args) = strip_comb lhs
     9.6        |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]);
     9.7 -    val (left_args, rest) = take_prefix is_Free args;
     9.8 -    val (nonfrees, right_args) = take_suffix is_Free rest;
     9.9 +    val (left_args, rest) = chop_prefix is_Free args;
    9.10 +    val (nonfrees, right_args) = chop_suffix is_Free rest;
    9.11      val num_nonfrees = length nonfrees;
    9.12      val _ = num_nonfrees = 1 orelse
    9.13        (if num_nonfrees = 0 then missing_pattern ctxt [eqn]
    10.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Jan 28 16:09:00 2018 +0100
    10.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Jan 28 19:28:52 2018 +0100
    10.3 @@ -75,7 +75,7 @@
    10.4            val _ $ Pxs = Logic.strip_assums_concl conc
    10.5            val (P, _) = strip_comb Pxs
    10.6            val (cases', conds) =
    10.7 -            take_prefix (Term.exists_subterm (curry op aconv P)) cases
    10.8 +            chop_prefix (Term.exists_subterm (curry op aconv P)) cases
    10.9            val concl' = fold_rev (curry Logic.mk_implies) conds conc
   10.10          in
   10.11            ([mk_branch concl'], cases')
   10.12 @@ -101,7 +101,7 @@
   10.13          fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
   10.14  
   10.15          val (gs, rcprs) =
   10.16 -          take_prefix (not o Term.exists_subterm is_pred) prems
   10.17 +          chop_prefix (not o Term.exists_subterm is_pred) prems
   10.18        in
   10.19          SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
   10.20            gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
    11.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Jan 28 16:09:00 2018 +0100
    11.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Jan 28 19:28:52 2018 +0100
    11.3 @@ -730,7 +730,7 @@
    11.4  (*This version does only one inference per call;
    11.5    having only one eq_assume_tac speeds it up!*)
    11.6  fun prolog_step_tac' ctxt horns =
    11.7 -    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
    11.8 +    let val horn0s = (*0 subgoals vs 1 or more*)
    11.9              take_prefix Thm.no_prems horns
   11.10          val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
   11.11      in  fn i => eq_assume_tac i ORELSE
    12.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jan 28 16:09:00 2018 +0100
    12.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jan 28 19:28:52 2018 +0100
    12.3 @@ -49,8 +49,8 @@
    12.4            else primrec_error "illegal head of function equation"
    12.5        | _ => primrec_error "illegal head of function equation");
    12.6  
    12.7 -    val (ls', rest)  = take_prefix is_Free args;
    12.8 -    val (middle, rs') = take_suffix is_Free rest;
    12.9 +    val (ls', rest)  = chop_prefix is_Free args;
   12.10 +    val (middle, rs') = chop_suffix is_Free rest;
   12.11      val rpos = length ls';
   12.12  
   12.13      val (constr, cargs') =
    13.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jan 28 16:09:00 2018 +0100
    13.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jan 28 19:28:52 2018 +0100
    13.3 @@ -202,7 +202,7 @@
    13.4                        (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
    13.5                      Quickcheck.message ctxt
    13.6                        "Quickcheck continues to find a genuine counterexample...";
    13.7 -                    test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
    13.8 +                    test true (drop_prefix (fn x => not (x = (card, size))) enum)
    13.9                  end
   13.10              | NONE => ())
   13.11          in (test genuine_only enumeration_card_size; !current_result) end)
    14.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 28 16:09:00 2018 +0100
    14.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 28 19:28:52 2018 +0100
    14.3 @@ -94,7 +94,7 @@
    14.4        SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
    14.5      val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
    14.6  
    14.7 -    val output = fst (take_suffix (equal "") res)
    14.8 +    val output = drop_suffix (equal "") res
    14.9      val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
   14.10  
   14.11      val _ = member (op =) normal_return_codes return_code orelse
    15.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Sun Jan 28 16:09:00 2018 +0100
    15.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Sun Jan 28 19:28:52 2018 +0100
    15.3 @@ -33,7 +33,7 @@
    15.4  fun on_first_line test_outcome solver_name lines =
    15.5    let
    15.6      val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    15.7 -    val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
    15.8 +    val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
    15.9    in (test_outcome solver_name l, ls) end
   15.10  
   15.11  fun on_first_non_unsupported_line test_outcome solver_name lines =
    16.1 --- a/src/HOL/Tools/SMT/smtlib.ML	Sun Jan 28 16:09:00 2018 +0100
    16.2 +++ b/src/HOL/Tools/SMT/smtlib.ML	Sun Jan 28 19:28:52 2018 +0100
    16.3 @@ -40,7 +40,7 @@
    16.4  (* utilities *)
    16.5  
    16.6  fun read_raw pred l cs =
    16.7 -  (case take_prefix pred cs of
    16.8 +  (case chop_prefix pred cs of
    16.9      ([], []) => raise PARSE (l, "empty token")
   16.10    | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
   16.11    | x => x)
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 16:09:00 2018 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 19:28:52 2018 +0100
    17.3 @@ -362,7 +362,7 @@
    17.4          Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
    17.5      val (perfect, imperfect) = candidates
    17.6        |> sort (Real.compare o swap o apply2 snd)
    17.7 -      |> take_prefix (fn (_, w) => w > 0.99999)
    17.8 +      |> chop_prefix (fn (_, w) => w > 0.99999)
    17.9      val ((accepts, more_rejects), rejects) =
   17.10        chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   17.11    in
    18.1 --- a/src/HOL/Tools/sat_solver.ML	Sun Jan 28 16:09:00 2018 +0100
    18.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun Jan 28 19:28:52 2018 +0100
    18.3 @@ -307,7 +307,7 @@
    18.4        | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
    18.5      fun clauses xs =
    18.6        let
    18.7 -        val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
    18.8 +        val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs
    18.9        in
   18.10          case xs2 of
   18.11            []      => [xs1]
    19.1 --- a/src/Pure/General/antiquote.ML	Sun Jan 28 16:09:00 2018 +0100
    19.2 +++ b/src/Pure/General/antiquote.ML	Sun Jan 28 19:28:52 2018 +0100
    19.3 @@ -49,7 +49,7 @@
    19.4      fun add a (line, lines) = (a :: line, lines);
    19.5      fun flush (line, lines) = ([], rev line :: lines);
    19.6      fun split (a as Text ss) =
    19.7 -          (case take_prefix (fn ("\n", _) => false | _ => true) ss of
    19.8 +          (case chop_prefix (fn ("\n", _) => false | _ => true) ss of
    19.9              ([], []) => I
   19.10            | (_, []) => add a
   19.11            | ([], _ :: rest) => flush #> split (Text rest)
    20.1 --- a/src/Pure/General/path.ML	Sun Jan 28 16:09:00 2018 +0100
    20.2 +++ b/src/Pure/General/path.ML	Sun Jan 28 19:28:52 2018 +0100
    20.3 @@ -150,7 +150,7 @@
    20.4        handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
    20.5  
    20.6      val (roots, raw_elems) =
    20.7 -      (case take_prefix (equal "") (space_explode "/" str) |>> length of
    20.8 +      (case chop_prefix (equal "") (space_explode "/" str) |>> length of
    20.9          (0, es) => ([], es)
   20.10        | (1, es) => ([Root ""], es)
   20.11        | (_, []) => ([Root ""], [])
   20.12 @@ -190,7 +190,7 @@
   20.13    | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
   20.14  
   20.15  val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   20.16 -  (case take_suffix (fn c => c <> ".") (raw_explode s) of
   20.17 +  (case chop_suffix (fn c => c <> ".") (raw_explode s) of
   20.18      ([], _) => (Path [Basic s], "")
   20.19    | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
   20.20  
    21.1 --- a/src/Pure/General/pretty.ML	Sun Jan 28 16:09:00 2018 +0100
    21.2 +++ b/src/Pure/General/pretty.ML	Sun Jan 28 19:28:52 2018 +0100
    21.3 @@ -128,7 +128,7 @@
    21.4      val indent' = force_nat indent;
    21.5      fun body_length prts len =
    21.6        let
    21.7 -        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
    21.8 +        val (line, rest) = chop_prefix (fn Break (true, _, _) => false | _ => true) prts;
    21.9          val len' = Int.max (fold (Integer.add o length) line 0, len);
   21.10        in
   21.11          (case rest of
    22.1 --- a/src/Pure/General/symbol.ML	Sun Jan 28 16:09:00 2018 +0100
    22.2 +++ b/src/Pure/General/symbol.ML	Sun Jan 28 19:28:52 2018 +0100
    22.3 @@ -199,7 +199,7 @@
    22.4  
    22.5  fun beginning n cs =
    22.6    let
    22.7 -    val drop_blanks = #1 o take_suffix is_ascii_blank;
    22.8 +    val drop_blanks = drop_suffix is_ascii_blank;
    22.9      val all_cs = drop_blanks cs;
   22.10      val dots = if length all_cs > n then " ..." else "";
   22.11    in
   22.12 @@ -465,7 +465,7 @@
   22.13            then chr (ord s + 1) :: ss
   22.14            else "a" :: s :: ss;
   22.15  
   22.16 -    val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
   22.17 +    val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
   22.18      val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   22.19    in implode (rev ss' @ qs) end;
   22.20  
    23.1 --- a/src/Pure/Isar/code.ML	Sun Jan 28 16:09:00 2018 +0100
    23.2 +++ b/src/Pure/Isar/code.ML	Sun Jan 28 19:28:52 2018 +0100
    23.3 @@ -1380,7 +1380,7 @@
    23.4  
    23.5  fun subsumptive_add thy verbose (thm, proper) eqns =
    23.6    let
    23.7 -    val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
    23.8 +    val args_of = drop_prefix is_Var o rev o snd o strip_comb
    23.9        o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
   23.10      val args = args_of thm;
   23.11      val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
    24.1 --- a/src/Pure/Isar/element.ML	Sun Jan 28 16:09:00 2018 +0100
    24.2 +++ b/src/Pure/Isar/element.ML	Sun Jan 28 19:28:52 2018 +0100
    24.3 @@ -233,7 +233,7 @@
    24.4      val concl_term = Object_Logic.drop_judgment ctxt concl;
    24.5  
    24.6      val (assumes, cases) =
    24.7 -      take_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    24.8 +      chop_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    24.9      val is_thesis = if null cases then K false else fn v => v aconv concl_term;
   24.10      val fixes =
   24.11        rev (fold_aterms (fn v as Free (x, T) =>
    25.1 --- a/src/Pure/Isar/proof.ML	Sun Jan 28 16:09:00 2018 +0100
    25.2 +++ b/src/Pure/Isar/proof.ML	Sun Jan 28 19:28:52 2018 +0100
    25.3 @@ -975,7 +975,7 @@
    25.4  
    25.5  fun implicit_vars props =
    25.6    let
    25.7 -    val (var_props, _) = take_prefix is_var props;
    25.8 +    val var_props = take_prefix is_var props;
    25.9      val explicit_vars = fold Term.add_vars var_props [];
   25.10      val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
   25.11    in map (Logic.mk_term o Var) vars end;
    26.1 --- a/src/Pure/Isar/proof_context.ML	Sun Jan 28 16:09:00 2018 +0100
    26.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Jan 28 19:28:52 2018 +0100
    26.3 @@ -1536,7 +1536,7 @@
    26.4      val print_name = Token.print_name (Thy_Header.get_keywords' ctxt);
    26.5  
    26.6      fun trim_name x = if Name.is_internal x then Name.clean x else "_";
    26.7 -    val trim_names = map trim_name #> take_suffix (equal "_") #> #1;
    26.8 +    val trim_names = map trim_name #> drop_suffix (equal "_");
    26.9  
   26.10      fun print_case name xs =
   26.11        (case trim_names xs of
    27.1 --- a/src/Pure/PIDE/command.ML	Sun Jan 28 16:09:00 2018 +0100
    27.2 +++ b/src/Pure/PIDE/command.ML	Sun Jan 28 19:28:52 2018 +0100
    27.3 @@ -131,7 +131,7 @@
    27.4    let
    27.5      val command_reports = Outer_Syntax.command_reports thy;
    27.6  
    27.7 -    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
    27.8 +    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
    27.9      val pos =
   27.10        (case find_first Token.is_command span of
   27.11          SOME tok => Token.pos_of tok
    28.1 --- a/src/Pure/Proof/extraction.ML	Sun Jan 28 16:09:00 2018 +0100
    28.2 +++ b/src/Pure/Proof/extraction.ML	Sun Jan 28 19:28:52 2018 +0100
    28.3 @@ -70,7 +70,7 @@
    28.4    | rlz_proc _ = NONE;
    28.5  
    28.6  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
    28.7 -  take_prefix (fn s => s <> ":") o raw_explode;
    28.8 +  chop_prefix (fn s => s <> ":") o raw_explode;
    28.9  
   28.10  type rules =
   28.11    {next: int, rs: ((term * term) list * (term * term)) list,
    29.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Jan 28 16:09:00 2018 +0100
    29.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 28 19:28:52 2018 +0100
    29.3 @@ -406,7 +406,7 @@
    29.4    let
    29.5      val cs = Symbol.explode str;
    29.6      val (intpart, fracpart) =
    29.7 -      (case take_prefix Symbol.is_digit cs of
    29.8 +      (case chop_prefix Symbol.is_digit cs of
    29.9          (intpart, "." :: fracpart) => (intpart, fracpart)
   29.10        | _ => raise Fail "read_float");
   29.11    in
    30.1 --- a/src/Pure/Thy/markdown.ML	Sun Jan 28 16:09:00 2018 +0100
    30.2 +++ b/src/Pure/Thy/markdown.ML	Sun Jan 28 19:28:52 2018 +0100
    30.3 @@ -90,7 +90,7 @@
    30.4  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    30.5  
    30.6  fun strip_spaces (Antiquote.Text ss :: rest) =
    30.7 -      let val (sp, ss') = take_prefix is_space ss
    30.8 +      let val (sp, ss') = chop_prefix is_space ss
    30.9        in (length sp, if null ss' then rest else Antiquote.Text ss' :: rest) end
   30.10    | strip_spaces source = (0, source);
   30.11  
   30.12 @@ -149,7 +149,7 @@
   30.13  
   30.14  fun list_items [] = []
   30.15    | list_items (item :: rest) =
   30.16 -      let val (item_rest, rest') = take_prefix (not o is_item) rest;
   30.17 +      let val (item_rest, rest') = chop_prefix (not o is_item) rest;
   30.18        in (item :: item_rest) :: list_items rest' end;
   30.19  
   30.20  
    31.1 --- a/src/Pure/Thy/thy_output.ML	Sun Jan 28 16:09:00 2018 +0100
    31.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Jan 28 19:28:52 2018 +0100
    31.3 @@ -209,16 +209,16 @@
    31.4  
    31.5  fun make_span cmd src =
    31.6    let
    31.7 -    fun take_newline (tok :: toks) =
    31.8 +    fun chop_newline (tok :: toks) =
    31.9            if newline_token (fst tok) then ([tok], toks, true)
   31.10            else ([], tok :: toks, false)
   31.11 -      | take_newline [] = ([], [], false);
   31.12 +      | chop_newline [] = ([], [], false);
   31.13      val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
   31.14        src
   31.15 -      |> take_prefix (white_token o fst)
   31.16 -      ||>> take_suffix (white_token o fst)
   31.17 -      ||>> take_prefix (white_comment_token o fst)
   31.18 -      ||> take_newline;
   31.19 +      |> chop_prefix (white_token o fst)
   31.20 +      ||>> chop_suffix (white_token o fst)
   31.21 +      ||>> chop_prefix (white_comment_token o fst)
   31.22 +      ||> chop_newline;
   31.23    in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
   31.24  
   31.25  
   31.26 @@ -405,7 +405,7 @@
   31.27            make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   31.28  
   31.29      val spans = toks
   31.30 -      |> take_suffix Token.is_space |> #1
   31.31 +      |> drop_suffix Token.is_space
   31.32        |> Source.of_list
   31.33        |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
   31.34        |> Source.source stopper (Scan.error (Scan.bulk span))
    32.1 --- a/src/Pure/library.ML	Sun Jan 28 16:09:00 2018 +0100
    32.2 +++ b/src/Pure/library.ML	Sun Jan 28 19:28:52 2018 +0100
    32.3 @@ -99,9 +99,13 @@
    32.4    val ~~ : 'a list * 'b list -> ('a * 'b) list
    32.5    val split_list: ('a * 'b) list -> 'a list * 'b list
    32.6    val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
    32.7 +  val take_prefix: ('a -> bool) -> 'a list -> 'a list
    32.8 +  val drop_prefix: ('a -> bool) -> 'a list -> 'a list
    32.9 +  val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   32.10 +  val take_suffix: ('a -> bool) -> 'a list -> 'a list
   32.11 +  val drop_suffix: ('a -> bool) -> 'a list -> 'a list
   32.12 +  val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   32.13    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   32.14 -  val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   32.15 -  val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   32.16    val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   32.17    val prefixes1: 'a list -> 'a list list
   32.18    val prefixes: 'a list -> 'a list list
   32.19 @@ -526,28 +530,53 @@
   32.20  fun burrow_fst f xs = split_list xs |>> f |> op ~~;
   32.21  
   32.22  
   32.23 +(* take, drop, chop, trim according to predicate *)
   32.24 +
   32.25 +fun take_prefix pred list =
   32.26 +  let
   32.27 +    fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res
   32.28 +      | take res [] = rev res;
   32.29 +  in take [] list end;
   32.30 +
   32.31 +fun drop_prefix pred list =
   32.32 +  let
   32.33 +    fun drop (x :: xs) = if pred x then drop xs else x :: xs
   32.34 +      | drop [] = [];
   32.35 +  in drop list end;
   32.36 +
   32.37 +fun chop_prefix pred list =
   32.38 +  let
   32.39 +    val prfx = take_prefix pred list;
   32.40 +    val sffx = drop (length prfx) list;
   32.41 +  in (prfx, sffx) end;
   32.42 +
   32.43 +fun take_suffix pred list =
   32.44 +  let
   32.45 +    fun take res (x :: xs) = if pred x then take (x :: res) xs else res
   32.46 +      | take res [] = res;
   32.47 +  in take [] (rev list) end;
   32.48 +
   32.49 +fun drop_suffix pred list =
   32.50 +  let
   32.51 +    fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs)
   32.52 +      | drop [] = [];
   32.53 +  in drop (rev list) end;
   32.54 +
   32.55 +fun chop_suffix pred list =
   32.56 +  let
   32.57 +    val prfx = drop_suffix pred list;
   32.58 +    val sffx = drop (length prfx) list;
   32.59 +  in (prfx, sffx) end;
   32.60 +
   32.61 +fun trim pred = drop_prefix pred #> drop_suffix pred;
   32.62 +
   32.63 +
   32.64  (* prefixes, suffixes *)
   32.65  
   32.66  fun is_prefix _ [] _ = true
   32.67    | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys
   32.68    | is_prefix eq _ _ = false;
   32.69  
   32.70 -(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., x(i-1)], [xi, ..., xn])
   32.71 -   where xi is the first element that does not satisfy the predicate*)
   32.72 -fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
   32.73 -  let fun take (rxs, []) = (rev rxs, [])
   32.74 -        | take (rxs, x :: xs) =
   32.75 -            if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
   32.76 -  in  take([], xs)  end;
   32.77 -
   32.78 -(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
   32.79 -   where xi is the last element that does not satisfy the predicate*)
   32.80 -fun take_suffix _ [] = ([], [])
   32.81 -  | take_suffix pred (x :: xs) =
   32.82 -      (case take_suffix pred xs of
   32.83 -        ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
   32.84 -      | (prfx, sffx) => (x :: prfx, sffx));
   32.85 -
   32.86  fun chop_common_prefix eq ([], ys) = ([], ([], ys))
   32.87    | chop_common_prefix eq (xs, []) = ([], (xs, []))
   32.88    | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
   32.89 @@ -564,8 +593,6 @@
   32.90  fun suffixes1 xs = map rev (prefixes1 (rev xs));
   32.91  fun suffixes xs = [] :: suffixes1 xs;
   32.92  
   32.93 -fun trim pred = take_prefix pred #> #2 #> take_suffix pred #> #1;
   32.94 -
   32.95  
   32.96  (** integers **)
   32.97  
    33.1 --- a/src/Tools/case_product.ML	Sun Jan 28 16:09:00 2018 +0100
    33.2 +++ b/src/Tools/case_product.ML	Sun Jan 28 19:28:52 2018 +0100
    33.3 @@ -48,8 +48,8 @@
    33.4      val concl = Thm.concl_of thm1
    33.5  
    33.6      fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
    33.7 -    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
    33.8 -    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
    33.9 +    val (p_cons1, p_cases1) = chop_prefix is_consumes (Thm.prems_of thm1)
   33.10 +    val (p_cons2, p_cases2) = chop_prefix is_consumes (Thm.prems_of thm2)
   33.11  
   33.12      val p_cases_prod = map (fn p1 => map (fn p2 =>
   33.13        let
    34.1 --- a/src/Tools/coherent.ML	Sun Jan 28 16:09:00 2018 +0100
    34.2 +++ b/src/Tools/coherent.ML	Sun Jan 28 19:28:52 2018 +0100
    34.3 @@ -54,8 +54,7 @@
    34.4    let
    34.5      val prems = Logic.strip_imp_prems prop;
    34.6      val concl = Logic.strip_imp_concl prop;
    34.7 -    val (prems1, prems2) =
    34.8 -      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
    34.9 +    val (prems1, prems2) = chop_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
   34.10    in
   34.11      (prems1,
   34.12       if null prems2 then [([], [concl])]
    35.1 --- a/src/ZF/Tools/primrec_package.ML	Sun Jan 28 16:09:00 2018 +0100
    35.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun Jan 28 19:28:52 2018 +0100
    35.3 @@ -40,8 +40,8 @@
    35.4      val (fname, ftype) = dest_Const recfun handle TERM _ =>
    35.5        raise RecError "function is not declared as constant in theory";
    35.6  
    35.7 -    val (ls_frees, rest)  = take_prefix is_Free args;
    35.8 -    val (middle, rs_frees) = take_suffix is_Free rest;
    35.9 +    val (ls_frees, rest)  = chop_prefix is_Free args;
   35.10 +    val (middle, rs_frees) = chop_suffix is_Free rest;
   35.11  
   35.12      val (constr, cargs_frees) =
   35.13        if null middle then raise RecError "constructor missing"