From d593972beacb3909f357223e4b31d934647d8185 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Tue, 26 Mar 2024 20:13:27 +1030
Subject: [PATCH] rename variables for rsubst2 squash

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Lib.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Lib.thy b/lib/Lib.thy
index cf43a02c5d..c658531f36 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -2536,7 +2536,7 @@ qed
 lemmas rsubst = back_subst[where a=s and b=t for s t]
 
 lemma rsubst2:
-  "\<lbrakk>P s x; s = t; x = y\<rbrakk> \<Longrightarrow> P t y"
+  "\<lbrakk>P a b; a = s; b = t\<rbrakk> \<Longrightarrow> P s t"
   by simp
 
 lemma rsubst3: