diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Tue Jan 21 19:26:39 2025 +0100
@@ -59,8 +59,8 @@
     val vname = singleton (Name.variant_list (map fst
       (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
     val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
-    val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
-    val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
+    val lhs_of = Thm.dest_arg1 o Thm.cprop_of;
+    val rhs_of = Thm.dest_arg o Thm.cprop_of;
     fun find_vars ct = (case Thm.term_of ct of
         (Const (\<^const_name>\<open>Suc\<close>, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
       | _ $ _ =>