--- 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))]
| _ $ _ =>