--- 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>