diff -r e0cd537c4325 -r 73069e033a0b src/HOL/Induct/QuoDataType.thy
--- 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')"