--- 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) =