diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -8,7 +8,7 @@
 imports Multiset
 begin
 
-inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  ("_ <~~> _"  [50, 50] 50)  (* FIXME proper infix, without ambiguity!? *)
+inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (\<open>_ <~~> _\<close>  [50, 50] 50)  (* FIXME proper infix, without ambiguity!? *)
 where
   Nil [intro!]: "[] <~~> []"
 | swap [intro!]: "y # x # l <~~> x # y # l"