equal
deleted
inserted
replaced
11 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
11 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
12 |
12 |
13 (* info of raw binding functions *) |
13 (* info of raw binding functions *) |
14 type bn_info = term * int * (int * term option) list list |
14 type bn_info = term * int * (int * term option) list list |
15 |
15 |
16 |
|
17 (* binding modes and binding clauses *) |
16 (* binding modes and binding clauses *) |
18 datatype bmode = Lst | Res | Set |
17 datatype bmode = Lst | Res | Set |
19 datatype bclause = BC of bmode * (term option * int) list * int list |
18 datatype bclause = BC of bmode * (term option * int) list * int list |
|
19 |
|
20 val get_all_binders: bclause list -> (term option * int) list |
20 |
21 |
21 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
22 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
22 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
23 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
23 (term list * thm list * bn_info list * thm list * local_theory) |
24 (term list * thm list * bn_info list * thm list * local_theory) |
24 |
25 |
54 type bn_info = term * int * (int * term option) list list |
55 type bn_info = term * int * (int * term option) list list |
55 |
56 |
56 |
57 |
57 datatype bmode = Lst | Res | Set |
58 datatype bmode = Lst | Res | Set |
58 datatype bclause = BC of bmode * (term option * int) list * int list |
59 datatype bclause = BC of bmode * (term option * int) list * int list |
|
60 |
|
61 fun get_all_binders bclauses = |
|
62 bclauses |
|
63 |> map (fn (BC (_, x, _)) => x) |
|
64 |> flat |
|
65 |> remove_dups (op =) |
59 |
66 |
60 fun lookup xs x = the (AList.lookup (op=) xs x) |
67 fun lookup xs x = the (AList.lookup (op=) xs x) |
61 |
68 |
62 |
69 |
63 (** functions that define the raw binding functions **) |
70 (** functions that define the raw binding functions **) |