src/HOL/BNF/Tools/bnf_util.ML
changeset 51757 7babcb61aa5c
parent 49835 31f32ec4d766
child 51758 55963309557b
     1.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:20 2013 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    val splice: 'a list -> 'a list -> 'a list
     1.5    val transpose: 'a list list -> 'a list list
     1.6    val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
     1.7 +  val pad_list: 'a -> int -> 'a list -> 'a list
     1.8  
     1.9    val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    1.10    val mk_TFrees: int -> Proof.context -> typ list * Proof.context
    1.11 @@ -616,6 +617,8 @@
    1.12        map (f false) negs @ [f true pos]
    1.13      end;
    1.14  
    1.15 +fun pad_list x n xs = xs @ replicate (n - length xs) x;
    1.16 +
    1.17  fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
    1.18  
    1.19  fun is_triv_implies thm =