changeset 27159 | 9506c7e73cfa |
parent 24123 | a0fc58900606 |
child 27225 | b316dde851f5 |
--- a/src/HOL/SET-Protocol/EventSET.thy Wed Jun 11 18:04:02 2008 +0200 +++ b/src/HOL/SET-Protocol/EventSET.thy Wed Jun 11 18:15:36 2008 +0200 @@ -180,7 +180,7 @@ ML {* val analz_mono_contra_tac = - let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI + let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI in rtac analz_impI THEN' REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN' mp_tac