diff -r fe9932a7cd46 -r e694c660055b src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Mon Oct 13 12:48:42 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Mon Oct 13 12:51:51 1997 +0200
@@ -36,7 +36,7 @@
  rsch_def "rsch == snd o snd o snd"
 
 hdr_sum_def
-   "hdr_sum M b == countm M (%pkt.hdr(pkt) = b)"
+   "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
 
 (* Lemma 5.1 *)
 inv1_def