src/HOL/Algebra/ringsimp.ML

--- a/src/HOL/Algebra/ringsimp.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -26,7 +26,6 @@
        identifier of the structure, list of operations and simp rules,
        identifier and operations identify the structure uniquely. *)
   val empty = [];
-  val extend = I;
   val merge = AList.join struct_eq (K Thm.merge_thms);
 );