diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -95,7 +95,6 @@
   type T = code_options
   val empty = {ensure_groundness = false, limit_globally = NONE,
     limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
-  val extend = I;
   fun merge
     ({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
       limited_types = limited_types1, limited_predicates = limited_predicates1,