--- a/src/HOL/Metis_Examples/Message.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Tue Feb 23 16:25:08 2016 +0100
@@ -460,7 +460,7 @@
by (intro equalityI lemma1 lemma2)
text{*Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
+but can cause subgoals to blow up! Use with @{text "if_split"}; apparently
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
(Crypt K X) H)"} *}
lemma analz_Crypt_if [simp]: