| changeset 74561 | 8e6c973003c8 |
| parent 69576 | cfac69e7b962 |
| child 76058 | d45a45eb1aee |
| 74560:5c8177fd1295 | 74561:8e6c973003c8 |
|---|---|
134 |
134 |
135 structure Data = Generic_Data |
135 structure Data = Generic_Data |
136 ( |
136 ( |
137 type T = value Inttab.table; |
137 type T = value Inttab.table; |
138 val empty = Inttab.empty; |
138 val empty = Inttab.empty; |
139 val extend = I; |
|
140 fun merge data = Inttab.merge (K true) data; |
139 fun merge data = Inttab.merge (K true) data; |
141 ); |
140 ); |
142 |
141 |
143 fun declare (name, pos) default = |
142 fun declare (name, pos) default = |
144 let |
143 let |