1.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -749,7 +749,7 @@
     1.4   (*SR9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
     1.5   (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
     1.6   (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
     1.7 - (*Base*)  (force_tac (clasimpset_of ctxt)) 1
     1.8 + (*Base*)  (force_tac ctxt) 1
     1.9  
    1.10  val analz_prepare_tac = 
    1.11           prepare_tac THEN