src/Tools/IsaPlanner/rw_inst.ML
changeset 74266 612b7e0d6721
parent 74233 9eff7c673b42
child 74282 c2ee8d993d6a
--- 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;