--- a/src/HOL/ex/Datatype_Record_Examples.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/Datatype_Record_Examples.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -22,7 +22,7 @@
 
 lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" ..
 
-local_setup \<open>Datatype_Records.mk_update_defs @{type_name x}\<close>
+local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>x\<close>\<close>
 
 lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3"
   by (simp add: datatype_record_update)