--- a/src/HOL/BNF/Tools/bnf_util.ML Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Apr 24 18:49:52 2013 +0200
@@ -43,6 +43,9 @@
val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
'j list * 'i
+ val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j -> 'k list * 'j
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
@@ -286,6 +289,15 @@
in (x :: xs, acc'') end
| fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
+ | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) acc =
+ let
+ val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
+ val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
+ in (x :: xs, acc'') end
+ | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);