--- 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}