equal
deleted
inserted
replaced
7 |
7 |
8 signature BNF_UTIL = |
8 signature BNF_UTIL = |
9 sig |
9 sig |
10 include CTR_SUGAR_UTIL |
10 include CTR_SUGAR_UTIL |
11 include BNF_FP_REC_SUGAR_UTIL |
11 include BNF_FP_REC_SUGAR_UTIL |
|
12 |
|
13 val unflatt: 'a list list list -> 'b list -> 'b list list list |
|
14 val unflattt: 'a list list list list -> 'b list -> 'b list list list list |
12 |
15 |
13 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
16 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
14 val mk_Freesss: string -> typ list list list -> Proof.context -> |
17 val mk_Freesss: string -> typ list list list -> Proof.context -> |
15 term list list list * Proof.context |
18 term list list list * Proof.context |
16 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
19 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
115 open Ctr_Sugar_Util |
118 open Ctr_Sugar_Util |
116 open BNF_FP_Rec_Sugar_Util |
119 open BNF_FP_Rec_Sugar_Util |
117 |
120 |
118 (* Library proper *) |
121 (* Library proper *) |
119 |
122 |
|
123 fun unfla0 xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs; |
|
124 fun unflat0 xss = fold_map unfla0 xss; |
|
125 fun unflatt0 xsss = fold_map unflat0 xsss; |
|
126 fun unflattt0 xssss = fold_map unflatt0 xssss; |
|
127 |
|
128 fun unflatt xsss = fst o unflatt0 xsss; |
|
129 fun unflattt xssss = fst o unflattt0 xssss; |
|
130 |
120 val parse_type_arg_constrained = |
131 val parse_type_arg_constrained = |
121 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
132 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
122 |
133 |
123 val parse_type_arg_named_constrained = |
134 val parse_type_arg_named_constrained = |
124 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |
135 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- |