src/Pure/library.ML

   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val prefixes1: 'a list -> 'a list list
   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
   val suffixes: 'a list -> 'a list list
+  val trim: ('a -> bool) -> 'a list -> 'a list
 
   (*integers*)
   val upto: int * int -> int list
   val downto: int * int -> int list
   val radixpand: int * int -> int list

 fun prefixes xs = [] :: prefixes1 xs;
 
 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 **)
 
 (* lists of integers *)