equal
deleted
inserted
replaced
16 (* binding modes and binding clauses *) |
16 (* binding modes and binding clauses *) |
17 datatype bmode = Lst | Res | Set |
17 datatype bmode = Lst | Res | Set |
18 datatype bclause = BC of bmode * (term option * int) list * int list |
18 datatype bclause = BC of bmode * (term option * int) list * int list |
19 |
19 |
20 val get_all_binders: bclause list -> (term option * int) list |
20 val get_all_binders: bclause list -> (term option * int) list |
|
21 val is_recursive_binder: bclause -> bool |
21 |
22 |
22 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
23 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
23 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
24 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
24 (term list * thm list * bn_info list * thm list * local_theory) |
25 (term list * thm list * bn_info list * thm list * local_theory) |
25 |
26 |
61 fun get_all_binders bclauses = |
62 fun get_all_binders bclauses = |
62 bclauses |
63 bclauses |
63 |> map (fn (BC (_, binders, _)) => binders) |
64 |> map (fn (BC (_, binders, _)) => binders) |
64 |> flat |
65 |> flat |
65 |> remove_dups (op =) |
66 |> remove_dups (op =) |
|
67 |
|
68 fun is_recursive_binder (BC (_, binders, bodies)) = |
|
69 case (inter (op =) (map snd binders) bodies) of |
|
70 nil => false |
|
71 | _ => true |
|
72 |
66 |
73 |
67 fun lookup xs x = the (AList.lookup (op=) xs x) |
74 fun lookup xs x = the (AList.lookup (op=) xs x) |
68 |
75 |
69 |
76 |
70 (** functions that define the raw binding functions **) |
77 (** functions that define the raw binding functions **) |