src/HOL/Tools/BNF/bnf_util.ML

   val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list *
     'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list
   val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list *
     'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
     'k list
+  val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) list -> 'a list *
+    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
+    'k list * 'l list
 
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
     term list list list * Proof.context
   val mk_Freessss: string -> typ list list list list -> Proof.context ->

   | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) =
     let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
         x9 :: xs9, x10 :: xs10, x11 :: xs11) end;
 
+fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], [])
+  | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12) end;
+
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
 val parse_type_arg_named_constrained =
    (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) --