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