diff -r ac158759125c -r b316dde851f5 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Mon Jun 16 14:18:55 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Mon Jun 16 17:54:35 2008 +0200
@@ -258,19 +258,16 @@
        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
 
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+
 ML
 {*
 val analz_mono_contra_tac = 
-  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
-  end
+  rtac @{thm analz_impI} THEN' 
+  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
+  THEN' mp_tac
 *}
 
-
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
 by (induct e, auto simp: knows_Cons)
 
@@ -295,6 +292,8 @@
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+
 ML
 {*
 val knows_Cons     = thm "knows_Cons"
@@ -334,17 +333,14 @@
 
 
 val synth_analz_mono_contra_tac = 
-  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
-  in
-    rtac syan_impI THEN' 
-    REPEAT1 o 
-      (dresolve_tac 
-       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
-        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
-	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
-    THEN'
-    mp_tac
-  end;
+  rtac @{thm syan_impI} THEN'
+  REPEAT1 o 
+    (dresolve_tac 
+     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
+      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
+      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
+  THEN'
+  mp_tac
 *}
 
 method_setup synth_analz_mono_contra = {*