reinserted legacy ML function

--- a/doc-src/TutorialI/Protocol/Message.thy	Tue Jul 28 13:37:09 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Tue Jul 28 13:37:40 2009 +0200
@@ -841,6 +841,8 @@
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 val Fake_insert_tac = 
     dresolve_tac [impOfSubs Fake_analz_insert,
                   impOfSubs Fake_parts_insert] THEN'