diff -r 56b6cdce22f1 -r 026f3db3f5c6 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -261,7 +261,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 
@@ -334,7 +334,7 @@
 
 
 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