
diff -r 1e29891759c4 -r dcfab8e87621 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Apr 12 15:30:38 2013 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Apr 12 17:02:55 2013 +0200
@@ -851,7 +851,6 @@
 {*
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
-  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
 fun impOfSubs th = th RSN (2, @{thm rev_subsetD})




