diff -r b3c65c984210 -r 1091880266e5 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -37,7 +37,7 @@
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;
-    val head_tfrees = Term_Subst.add_tfrees head Term_Subst.TFrees.empty;
+    val head_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfrees head);
 
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = check_free_lhs x