src/HOL/Auth/Event.thy
changeset 58963 26bf09b95dda
parent 58889 5b7a9633cfa8
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Auth/Event.thy	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -270,14 +270,14 @@
     1.4  
     1.5  ML
     1.6  {*
     1.7 -val analz_mono_contra_tac = 
     1.8 +fun analz_mono_contra_tac ctxt = 
     1.9    rtac @{thm analz_impI} THEN' 
    1.10    REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
    1.11 -  THEN' mp_tac
    1.12 +  THEN' (mp_tac ctxt)
    1.13  *}
    1.14  
    1.15  method_setup analz_mono_contra = {*
    1.16 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
    1.17 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
    1.18      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.19  
    1.20  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.21 @@ -286,7 +286,7 @@
    1.22  
    1.23  ML
    1.24  {*
    1.25 -val synth_analz_mono_contra_tac = 
    1.26 +fun synth_analz_mono_contra_tac ctxt = 
    1.27    rtac @{thm syan_impI} THEN'
    1.28    REPEAT1 o 
    1.29      (dresolve_tac 
    1.30 @@ -294,11 +294,11 @@
    1.31        @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.32        @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.33    THEN'
    1.34 -  mp_tac
    1.35 +  mp_tac ctxt
    1.36  *}
    1.37  
    1.38  method_setup synth_analz_mono_contra = {*
    1.39 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
    1.40 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
    1.41      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    1.42  
    1.43  end