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*)   clarify_tac (claset_of ctxt) 15 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 
 
 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                
- (*Base*)  (force_tac (clasimpset_of ctxt)) 1
+ (*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