37 | iter(Bound _, a) = a |
37 | iter(Bound _, a) = a |
38 in iter end |
38 in iter end |
39 |
39 |
40 (*Accumulates the names in the term, suppressing duplicates. |
40 (*Accumulates the names in the term, suppressing duplicates. |
41 Includes Frees and Consts. For choosing unambiguous bound var names.*) |
41 Includes Frees and Consts. For choosing unambiguous bound var names.*) |
42 fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs |
42 fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs |
43 | add_term_names (Free(a,_), bs) = insert (op =) a bs |
43 | add_term_names (Free(a,_), bs) = insert (op =) a bs |
44 | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) |
44 | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) |
45 | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) |
45 | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) |
46 | add_term_names (_, bs) = bs; |
46 | add_term_names (_, bs) = bs; |
47 |
47 |