diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -15,10 +15,10 @@
 (* messages  #replies        #received            header mode *)
 
 definition rq :: "'m receiver_state => 'm list" where "rq == fst"
-definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd"
-definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd"
-definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd"
-definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd"
+definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst \<circ> snd"
+definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst \<circ> snd \<circ> snd"
+definition rbit :: "'m receiver_state => bool" where "rbit == fst \<circ> snd \<circ> snd \<circ> snd"
+definition rsending :: "'m receiver_state => bool" where "rsending == snd \<circ> snd \<circ> snd \<circ> snd"
 
 definition
   receiver_asig :: "'m action signature" where