equal
deleted
inserted
replaced
58 datatype bmode = Lst | Res | Set |
58 datatype bmode = Lst | Res | Set |
59 datatype bclause = BC of bmode * (term option * int) list * int list |
59 datatype bclause = BC of bmode * (term option * int) list * int list |
60 |
60 |
61 fun get_all_binders bclauses = |
61 fun get_all_binders bclauses = |
62 bclauses |
62 bclauses |
63 |> map (fn (BC (_, x, _)) => x) |
63 |> map (fn (BC (_, binders, _)) => binders) |
64 |> flat |
64 |> flat |
65 |> remove_dups (op =) |
65 |> remove_dups (op =) |
66 |
66 |
67 fun lookup xs x = the (AList.lookup (op=) xs x) |
67 fun lookup xs x = the (AList.lookup (op=) xs x) |
68 |
68 |