--- a/src/HOL/Induct/QuoDataType.thy Thu Sep 02 14:50:00 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 02 16:52:21 2004 +0200
@@ -373,7 +373,7 @@
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
text{*...and many similar results*}
-theorem Crypt_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
+theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')"