src/Tools/IsaPlanner/rw_inst.ML

--- a/src/Tools/IsaPlanner/rw_inst.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat Sep 04 21:45:43 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' othertfrees
+    |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
     |-> K Drule.zero_var_indexes
   end;