diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -78,7 +78,7 @@
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
-   apply (metis parts.Inj set_rev_mp)
+   apply (metis parts.Inj rev_subsetD)
   apply (metis parts.Fst)
  apply (metis parts.Snd)
 by (metis parts.Body)