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>\_bound\, _) $ Free (v, Type (\<^type_name>\set\, _)), + (fn [Const (\<^syntax_const>\_bound\, _) $ Free (v, \<^Type>\set _\), Const (c, _) $ (Const (d, _) $ (Const (\<^syntax_const>\_bound\, _) $ Free (v', T)) $ n) $ P] => (case AList.lookup (=) trans (q, c, d) of