src/HOL/Auth/Event.thy

     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
 
 method_setup analz_mono_contra = {*
-    Method.no_args
-      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
+    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
 ML

     mp_tac
   end;
 *}
 
 method_setup synth_analz_mono_contra = {*
-    Method.no_args
-      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
 
 end