| changeset 1266 | 3ae9fe3c0f68 |
| parent 1051 | 4fcd0638e61d |
| child 1328 | 9a449a91425d |
--- a/src/HOL/IOA/NTP/Packet.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Packet.ML Wed Oct 04 13:12:14 1995 +0100 @@ -9,5 +9,5 @@ (* Instantiation of a tautology? *) goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)"; - by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1); + by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1); qed "eq_packet_imp_eq_hdr"; \ No newline at end of file