diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -35,7 +35,7 @@
 
 text \<open>
   If code generation fails with a message like
-  @{text \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>},
+  \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>,
   feel free to add an RBT implementation for the corrsponding operation
   of delete that code equation (see above).
 \<close>