--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 22:55:00 2011 +0200
@@ -748,7 +748,7 @@
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
@@ -758,7 +758,7 @@
(*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