src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Fun.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -154,7 +154,7 @@
 abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "surj f \<equiv> range f = UNIV"
 
-translations -- \<open>The negated case:\<close>
+translations \<comment> \<open>The negated case:\<close>
   "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
 
 abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"