--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy Sat Jan 08 00:28:31 2011 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy Sat Jan 08 09:30:52 2011 -0800 @@ -8,7 +8,7 @@ imports Main begin -types +type_synonym 'msg packet = "bool * 'msg" definition