57 val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) -> |
57 val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) -> |
58 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
58 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
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 * |
|
63 'e list * 'f list |
62 |
64 |
63 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
65 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
64 val mk_Freesss: string -> typ list list list -> Proof.context -> |
66 val mk_Freesss: string -> typ list list list -> Proof.context -> |
65 term list list list * Proof.context |
67 term list list list * Proof.context |
66 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
68 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
292 fun split_list5 [] = ([], [], [], [], []) |
294 fun split_list5 [] = ([], [], [], [], []) |
293 | split_list5 ((x1, x2, x3, x4, x5) :: xs) = |
295 | split_list5 ((x1, x2, x3, x4, x5) :: xs) = |
294 let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs; |
296 let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs; |
295 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end; |
297 in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end; |
296 |
298 |
|
299 fun split_list6 [] = ([], [], [], [], [], []) |
|
300 | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) = |
|
301 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; |
|
303 |
297 val parse_type_arg_constrained = |
304 val parse_type_arg_constrained = |
298 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
305 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
299 |
306 |
300 val parse_type_arg_named_constrained = |
307 val parse_type_arg_named_constrained = |
301 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |
308 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |