src/HOL/BNF/Tools/bnf_util.ML

   val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
+  val pad_list: 'a -> int -> 'a list -> 'a list
 
   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context

   else
     let val (negs, pos) = split_last (take k xs) in
       map (f false) negs @ [f true pos]
     end;
 
+fun pad_list x n xs = xs @ replicate (n - length xs) x;
+
 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
 fun is_triv_implies thm =
   op aconv (Logic.dest_implies (Thm.prop_of thm))
   handle TERM _ => false;