59 'i list -> 'j -> 'k list * 'j |
59 'i list -> 'j -> 'k list * 'j |
60 val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list |
60 val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list |
61 val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list |
61 val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list |
62 val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list * |
62 val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list * |
63 'e list * 'f list |
63 'e list * 'f list |
|
64 val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list * 'd list * |
|
65 'e list * 'f list * 'g list |
64 |
66 |
65 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
67 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
66 val mk_Freesss: string -> typ list list list -> Proof.context -> |
68 val mk_Freesss: string -> typ list list list -> Proof.context -> |
67 term list list list * Proof.context |
69 term list list list * Proof.context |
68 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
70 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
299 fun split_list6 [] = ([], [], [], [], [], []) |
301 fun split_list6 [] = ([], [], [], [], [], []) |
300 | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) = |
302 | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) = |
301 let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs; |
303 let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs; |
302 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end; |
304 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end; |
303 |
305 |
|
306 fun split_list7 [] = ([], [], [], [], [], [], []) |
|
307 | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) = |
|
308 let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs; |
|
309 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end; |
|
310 |
304 val parse_type_arg_constrained = |
311 val parse_type_arg_constrained = |
305 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
312 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
306 |
313 |
307 val parse_type_arg_named_constrained = |
314 val parse_type_arg_named_constrained = |
308 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |
315 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |