--- a/src/Tools/IsaPlanner/rw_inst.ML	Sat Apr 15 23:11:08 2023 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Mon Apr 17 23:32:46 2023 +0200
@@ -64,8 +64,7 @@
        bound vars with binders outside the redex *)
 
     val ns =
-      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Termset.dest (Thm.hyps_of rule))
-        (map fst Ts);
+      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
 
     val (fromnames, tonames, Ts') =
       fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>