diff -r 633fe7390c97 -r 612b7e0d6721 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -236,7 +236,7 @@
     |> Drule.implies_intr_list cprems
     |> Drule.forall_intr_list frees_of_fixed_vars
     |> Drule.forall_elim_list vars
-    |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
+    |> Thm.varifyT_global' (TFrees.make_set othertfrees)
     |-> K Drule.zero_var_indexes
   end;