src/HOL/ex/Tree23.thy

--- a/src/HOL/ex/Tree23.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Tree23.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -19,7 +19,7 @@
 function definitions take a few minutes and can also be seen as stress tests
 for the function definition facility.\<close>
 
-type_synonym key = int -- \<open>for simplicity, should be a type class\<close>
+type_synonym key = int \<comment> \<open>for simplicity, should be a type class\<close>
 
 datatype ord = LESS | EQUAL | GREATER