changeset 74561 | 8e6c973003c8 |
parent 74282 | c2ee8d993d6a |
child 77879 | dd222e2af01a |
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 20 18:13:17 2021 +0200 @@ -55,7 +55,6 @@ ( type T = nominal_datatype_info Symtab.table; val empty = Symtab.empty; - val extend = I; fun merge data = Symtab.merge (K true) data; );