src/HOL/HOLCF/ex/Pattern_Match.thy

     fun mk_tuple_pat [] = succeed_const \<^Type>\<open>unit\<close>
       | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
 
     (* 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
           val pat_bind = Binding.suffix_name "_pat" bind;
           val Ts = map snd args;

       val thy = Sign.add_trrules trans_rules thy;
     end;
 
     (* 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) =
         let
           val Ts = map snd args;