
diff -r 231d58c412b5 -r ad9647592a81 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/Set.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -251,7 +251,7 @@
       else raise Match;
 
     fun tr' q = (q, fn _ =>
-      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, Type (\<^type_name>\<open>set\<close>, _)),
+      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, \<^Type>\<open>set _\<close>),
           Const (c, _) $
             (Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
           (case AList.lookup (=) trans (q, c, d) of




