diff -r 231d58c412b5 -r ad9647592a81 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -199,12 +199,12 @@
   val Eq_TrueI = @{thm Eq_TrueI}
 
   fun is_subset A th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>less_eq\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>set\<close>, _), _])) $ A' $ B))
+        (_ $ \<^Const_>\<open>less_eq \<^Type>\<open>set _\<close> for A' B\<close>)
         => if A aconv A' then SOME(B,th) else NONE
       | _ => NONE;
 
   fun is_finite th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>finite\<close>, _) $ A)) => SOME(A,th)
+        (_ $ \<^Const_>\<open>finite _ for A\<close>) => SOME(A,th)
       |  _ => NONE;
 
   fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths