diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -1152,7 +1152,7 @@
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
 ML \<open>
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 \<close>