diff -r 8cff7900871f -r a123db647573 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -51,9 +51,10 @@
     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
       if check_free_rhs x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];
-    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
-      if check_tfree a orelse TFrees.defined head_tfrees (a, S) then I
-      else insert (op =) v | _ => I)) rhs [];
+    val rhs_extrasT =
+      TFrees.build (rhs |> TFrees.add_tfrees_unless
+        (fn (a, S) => check_tfree a orelse TFrees.defined head_tfrees (a, S)))
+      |> TFrees.list_set_rev |> map TFree;
   in
     if not (check_head head) then
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])