diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -44,17 +44,13 @@
 \<close>
 
 definition
-  conc :: "['a list, 'a word] \<Rightarrow> 'a word"    (infixr "conc" 65)
-  where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"
+  conc :: "['a list, 'a word] \<Rightarrow> 'a word"  (infixr "\<frown>" 65)
+  where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
 
 definition
-  iter :: "'a list \<Rightarrow> 'a word"
+  iter :: "'a list \<Rightarrow> 'a word"  ("(_\<^sup>\<omega>)" [1000])
   where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
 
-notation (xsymbols)
-  conc (infixr "\<frown>" 65) and
-  iter ("(_\<^sup>\<omega>)" [1000])
-
 lemma conc_empty[simp]: "[] \<frown> w = w"
   unfolding conc_def by auto