equal
deleted
inserted
replaced
92 val name = "HOL/datatypes"; |
92 val name = "HOL/datatypes"; |
93 type T = datatype_info Symtab.table; |
93 type T = datatype_info Symtab.table; |
94 |
94 |
95 val empty = Symtab.empty; |
95 val empty = Symtab.empty; |
96 val copy = I; |
96 val copy = I; |
97 val finish = I; |
|
98 val prep_ext = I; |
97 val prep_ext = I; |
99 val merge: T * T -> T = Symtab.merge (K true); |
98 val merge: T * T -> T = Symtab.merge (K true); |
100 |
99 |
101 fun print sg tab = |
100 fun print sg tab = |
102 Pretty.writeln (Pretty.strs ("datatypes:" :: |
101 Pretty.writeln (Pretty.strs ("datatypes:" :: |