changeset 74561 | 8e6c973003c8 |
parent 62923 | 3a122e1e352a |
child 78716 | 97dfba4405e3 |
--- a/src/Pure/Concurrent/thread_data_virtual.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/Pure/Concurrent/thread_data_virtual.ML Wed Oct 20 18:13:17 2021 +0200 @@ -11,7 +11,6 @@ ( type T = Universal.universal Inttab.table; val empty = Inttab.empty; - val extend = I; val merge = Inttab.merge (K true); );