--- 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,