diff -r 77cc7e7b50f2 -r 546d6d62aeab src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Jun 19 11:14:20 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Jun 19 11:20:36 1998 +0200
@@ -464,7 +464,7 @@
 
 (*Case analysis: either the message is secure, or it is not!
   Effective, but can cause subgoals to blow up!
-  Use with expand_if;  apparently split_tac does not cope with patterns
+  Use with split_if;  apparently split_tac does not cope with patterns
   such as "analz (insert (Crypt K X) H)" *)
 goal thy "analz (insert (Crypt K X) H) =                \
 \         (if (Key (invKey K) : analz H)                \