--- a/src/HOL/Auth/Event.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Auth/Event.thy Mon Nov 10 21:49:48 2014 +0100
@@ -270,14 +270,14 @@
ML
{*
-val analz_mono_contra_tac =
+fun analz_mono_contra_tac ctxt =
rtac @{thm analz_impI} THEN'
REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
- THEN' mp_tac
+ THEN' (mp_tac ctxt)
*}
method_setup analz_mono_contra = {*
- Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
"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*}
@@ -286,7 +286,7 @@
ML
{*
-val synth_analz_mono_contra_tac =
+fun synth_analz_mono_contra_tac ctxt =
rtac @{thm syan_impI} THEN'
REPEAT1 o
(dresolve_tac
@@ -294,11 +294,11 @@
@{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
@{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
THEN'
- mp_tac
+ mp_tac ctxt
*}
method_setup synth_analz_mono_contra = {*
- Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
"for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
end