src/HOL/Quotient_Examples/Quotient_FSet.thy

--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Sun Aug 11 20:19:47 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Sun Aug 11 20:20:05 2024 +0200
@@ -1147,7 +1147,7 @@
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
 ML \<open>
-fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T
+fun dest_fsetT \<^Type>\<open>fset T\<close> = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 \<close>