diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -1557,7 +1557,7 @@
                * term "f v1..vn" which is a pattern that any full application
                * of "f" will match.
                *-------------------------------------------------------------*)
-              val func_name = #1(dest_Const func)
+              val func_name = dest_Const_name func
               fun is_func (Const (name,_)) = (name = func_name)
                 | is_func _                = false
               val rcontext = rev cntxt
@@ -1730,7 +1730,7 @@
                fold_rev (fn (row as (p::rst, rhs)) =>
                          fn (in_group,not_in_group) =>
                   let val (pc,args) = USyntax.strip_comb p
-                  in if (#1(dest_Const pc) = c)
+                  in if (dest_Const_name pc = c)
                      then ((args@rst, rhs)::in_group, not_in_group)
                      else (in_group, row::not_in_group)
                   end)      rows ([],[])
@@ -1768,7 +1768,7 @@
  * Produce an instance of a constructor, plus genvars for its arguments.
  *---------------------------------------------------------------------------*)
 fun fresh_constr ty_match colty gv c =
-  let val (_,Ty) = dest_Const c
+  let val Ty = dest_Const_type c
       val L = binder_types Ty
       and ty = body_type Ty
       val ty_theta = ty_match ty colty
@@ -1786,7 +1786,7 @@
   fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
             fn (in_group,not_in_group) =>
                let val (pc,args) = USyntax.strip_comb p
-               in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
+               in if ((dest_Const_name pc = name) handle TERM _ => false)
                   then (((prfx,args@rst), rhs)::in_group, not_in_group)
                   else (in_group, row::not_in_group) end)
       rows ([],[]);
@@ -1801,7 +1801,7 @@
      fun part {constrs = [],      rows, A} = rev A
        | part {constrs = c::crst, rows, A} =
          let val (c',gvars) = fresh c
-             val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
+             val (in_group, not_in_group) = mk_group (dest_Const_name c') rows
              val in_group' =
                  if (null in_group)  (* Constructor not given *)
                  then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
@@ -1884,7 +1884,7 @@
      of NONE => mk_case_fail("Not a known datatype: "^ty_name)
       | SOME{case_const,constructors} =>
         let
-            val case_const_name = #1(dest_Const case_const)
+            val case_const_name = dest_Const_name case_const
             val nrows = maps (expand constructors pty) rows
             val subproblems = divide(constructors, pty, range_ty, nrows)
             val groups      = map #group subproblems
@@ -2701,7 +2701,7 @@
 local
 
 val cong_head =
-  fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
+  dest_Const_name o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
 
 fun prep_cong raw_thm =
   let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;