src/HOL/SET-Protocol/EventSET.thy

--- 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