diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Transfer.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -532,7 +532,12 @@
 
 lemma rec_nat_transfer [transfer_rule]:
   "(A ===> ((=) ===> A ===> A) ===> (=) ===> A) rec_nat rec_nat"
-  unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+  unfolding rel_fun_def
+  apply safe
+  subgoal for _ _ _ _ _ n
+    by (induction n) simp_all
+  done
+
 
 lemma funpow_transfer [transfer_rule]:
   "((=) ===> (A ===> A) ===> (A ===> A)) compow compow"