src/HOLCF/IOA/NTP/Packet.ML

--- a/src/HOLCF/IOA/NTP/Packet.ML	Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.ML	Sat Sep 03 16:50:22 2005 +0200
@@ -7,7 +7,7 @@
 
 (* Instantiation of a tautology? *)
 Goal "!x. x = packet --> hdr(x) = hdr(packet)";
- by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
+ by (simp_tac (simpset() addsimps [hdr_def]) 1);
 qed "eq_packet_imp_eq_hdr"; 
 
-Addsimps [Packet.hdr_def,Packet.msg_def];
+Addsimps [hdr_def,msg_def];