src/Pure/config.ML
changeset 74561 8e6c973003c8
parent 69576 cfac69e7b962
child 76058 d45a45eb1aee
--- a/src/Pure/config.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/config.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -136,7 +136,6 @@
 (
   type T = value Inttab.table;
   val empty = Inttab.empty;
-  val extend = I;
   fun merge data = Inttab.merge (K true) data;
 );