--- a/src/HOL/Auth/Event.thy Wed Jun 11 18:02:00 2008 +0200
+++ b/src/HOL/Auth/Event.thy Wed Jun 11 18:02:25 2008 +0200
@@ -281,7 +281,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
@@ -299,7 +299,7 @@
ML
{*
val synth_analz_mono_contra_tac =
- let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
+ let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
in
rtac syan_impI THEN'
REPEAT1 o