diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -280,7 +280,7 @@
     fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
     val revcut_rl' =
       Drule.revcut_rl |> Drule.instantiate_normalize
-        (TVars.empty, Vars.make [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]);
+        (TVars.empty, Vars.make2 (var "V", cvar ("V", maxidx + 1)) (var "W", cvar ("W", maxidx + 1)));
   in
     (case Seq.list_of
       (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}