--- a/src/HOL/IOA/ABP/Packet.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Packet.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -12,14 +12,12 @@
 
    'msg packet = "bool * 'msg"
 
-consts
+constdefs
 
   hdr  :: 'msg packet => bool
-  msg :: 'msg packet => 'msg
+  "hdr == fst"
 
-defs
-
-  hdr_def "hdr == fst"
-  msg_def "msg == snd"
+  msg :: 'msg packet => 'msg
+  "msg == snd"
 
 end