67 'd list * 'e list * 'f list * 'g list * 'h list |
67 'd list * 'e list * 'f list * 'g list * 'h list |
68 val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list * |
68 val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list * |
69 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list |
69 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list |
70 val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list * |
70 val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list * |
71 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list |
71 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list |
|
72 val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list * |
|
73 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list * |
|
74 'k list |
72 |
75 |
73 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
76 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
74 val mk_Freesss: string -> typ list list list -> Proof.context -> |
77 val mk_Freesss: string -> typ list list list -> Proof.context -> |
75 term list list list * Proof.context |
78 term list list list * Proof.context |
76 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
79 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
329 | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) = |
332 | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) = |
330 let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs; |
333 let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs; |
331 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, |
334 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, |
332 x9 :: xs9, x10 :: xs10) end; |
335 x9 :: xs9, x10 :: xs10) end; |
333 |
336 |
|
337 fun split_list11 [] = ([], [], [], [], [], [], [], [], [], [], []) |
|
338 | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) = |
|
339 let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs; |
|
340 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, |
|
341 x9 :: xs9, x10 :: xs10, x11 :: xs11) end; |
|
342 |
334 val parse_type_arg_constrained = |
343 val parse_type_arg_constrained = |
335 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
344 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
336 |
345 |
337 val parse_type_arg_named_constrained = |
346 val parse_type_arg_named_constrained = |
338 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |
347 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |