diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Aug 04 13:24:54 2024 +0200
@@ -461,7 +461,7 @@
 
     (* define pattern combinators *)
     local
-      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+      val tns = map (fst o dest_TFree) (dest_Type_args lhsT);
 
       fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
         let
@@ -527,7 +527,7 @@
 
     (* prove strictness and reduction rules of pattern combinators *)
     local
-      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+      val tns = map (fst o dest_TFree) (dest_Type_args lhsT);
       val rn = singleton (Name.variant_list tns) "'r";
       val R = TFree (rn, \<^sort>\<open>pcpo\<close>);
       fun pat_lhs (pat, args) =