# HG changeset patch
# User wenzelm
# Date 1723400405 -7200
# Node ID 3b6d84c32bfd6fef74da70f239c22d44634b5082
# Parent  58a209c8d40abbb90ff687334e3b0c4feed67470
tuned: more antiquotations;

diff -r 58a209c8d40a -r 3b6d84c32bfd 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>