--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:49 2014 +0200
@@ -81,6 +81,10 @@
val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) 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 * 'm list * 'n list
+ val split_list15:
+ ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o) 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 * 'm list * 'n list * 'o list
val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
val mk_Freesss: string -> typ list list list -> Proof.context ->
@@ -368,6 +372,14 @@
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, x13 :: xs13, x14 :: xs14) end;
+fun split_list15 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+ | split_list15 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) :: xs) =
+ let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14, xs15) =
+ split_list15 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, x13 :: xs13, x14 :: xs14, x15 :: xs15)
+ end;
+
val parse_type_arg_constrained =
Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);