diff -r 76ac4dbb0a22 -r d637611b41bd src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/variable.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -691,10 +691,10 @@
 
 fun focus_subgoal bindings i st =
   let
-    val all_vars = Thm.fold_terms Term.add_vars st [];
+    val all_vars = Thm.fold_terms Term_Subst.add_vars st Term_Subst.Vars.empty;
   in
-    fold (unbind_term o #1) all_vars #>
-    fold (declare_constraints o Var) all_vars #>
+    Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
+    Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
   end;