# HG changeset patch
# User paulson
# Date 898248036 -7200
# Node ID 546d6d62aeab59675f7e62b81395f7723cdf3af7
# Parent  77cc7e7b50f2b1734dc6a67c5513dd4c37d95305
fixed comment

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)                \