src/HOL/Auth/Smartcard/ShoupRubinBella.thy

 {*
 structure ShoupRubinBella =
 struct
 
 fun prepare_tac ctxt = 
- (*SR_U8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
+ (*SR_U8*)   forward_tac ctxt [@{thm Outpts_B_Card_form_7}] 14 THEN
  (*SR_U8*)   clarify_tac ctxt 15 THEN
- (*SR_U9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
- (*SR_U11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 
+ (*SR_U9*)   forward_tac ctxt [@{thm Outpts_A_Card_form_4}] 16 THEN 
+ (*SR_U11*)  forward_tac ctxt [@{thm Outpts_A_Card_form_10}] 21 
 
 fun parts_prepare_tac ctxt = 
            prepare_tac ctxt THEN
- (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
- (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
- (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
- (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
+ (*SR_U9*)   dresolve_tac ctxt [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
+ (*SR_U9*)   dresolve_tac ctxt [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
+ (*Oops1*) dresolve_tac ctxt [@{thm Outpts_B_Card_form_7}] 25    THEN               
+ (*Oops2*) dresolve_tac ctxt [@{thm Outpts_A_Card_form_10}] 27 THEN                
  (*Base*)  (force_tac ctxt) 1
 
 fun analz_prepare_tac ctxt = 
          prepare_tac ctxt THEN
          dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
  (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
-         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
+         REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
 
 end
 *}
 
 method_setup prepare = {*

 done
 
 method_setup sc_analz_freshK = {*
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
               addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
                   @{thm knows_Spy_Outpts_secureM_srb_Spy},
                   @{thm shouprubin_assumes_securemeans},