--- a/src/HOL/Auth/Message.thy Fri Feb 18 15:17:39 2011 +0100 +++ b/src/HOL/Auth/Message.thy Fri Feb 18 15:46:13 2011 +0100 @@ -16,7 +16,7 @@ lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" by blast -types +type_synonym key = nat consts