equal
deleted
inserted
replaced
94 structure TFrees: |
94 structure TFrees: |
95 sig |
95 sig |
96 include TERM_ITEMS |
96 include TERM_ITEMS |
97 val add_tfreesT: typ -> set -> set |
97 val add_tfreesT: typ -> set -> set |
98 val add_tfrees: term -> set -> set |
98 val add_tfrees: term -> set -> set |
|
99 val add_tfreesT_unless: (string * sort -> bool) -> typ -> set -> set |
|
100 val add_tfrees_unless: (string * sort -> bool) -> term -> set -> set |
99 end = |
101 end = |
100 struct |
102 struct |
101 |
103 |
102 structure Items = Term_Items |
104 structure Items = Term_Items |
103 ( |
105 ( |
106 ); |
108 ); |
107 open Items; |
109 open Items; |
108 |
110 |
109 val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I); |
111 val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I); |
110 val add_tfrees = fold_types add_tfreesT; |
112 val add_tfrees = fold_types add_tfreesT; |
|
113 |
|
114 fun add_tfreesT_unless pred = Term.fold_atyps (fn TFree v => not (pred v) ? add_set v | _ => I); |
|
115 fun add_tfrees_unless pred = fold_types (add_tfreesT_unless pred); |
111 |
116 |
112 end; |
117 end; |
113 |
118 |
114 |
119 |
115 structure TVars: |
120 structure TVars: |