--- a/src/Pure/ML/ml_env.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/Pure/ML/ml_env.ML Wed Oct 20 18:13:17 2021 +0200 @@ -117,7 +117,6 @@ ( type T = data; val empty = empty_data; - val extend = I; val merge = merge_data; );