diff -r ac158759125c -r b316dde851f5 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 14:18:55 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 17:54:35 2008 +0200
@@ -787,20 +787,22 @@
 
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
-ML
-{*
-fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
-bind_thms ("pushKeys",
-           map (insComm "Key ?K") 
-                   ["Agent ?C", "Nonce ?N", "Number ?N", 
-		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
+lemmas pushKeys [standard] =
+  insert_commute [of "Key K" "Agent C"]
+  insert_commute [of "Key K" "Nonce N"]
+  insert_commute [of "Key K" "Number N"]
+  insert_commute [of "Key K" "Hash X"]
+  insert_commute [of "Key K" "MPair X Y"]
+  insert_commute [of "Key K" "Crypt X K'"]
 
-bind_thms ("pushCrypts",
-           map (insComm "Crypt ?X ?K") 
-                     ["Agent ?C", "Nonce ?N", "Number ?N", 
-		      "Hash ?X'", "MPair ?X' ?Y"]);
-*}
+lemmas pushCrypts [standard] =
+  insert_commute [of "Crypt X K" "Agent C"]
+  insert_commute [of "Crypt X K" "Agent C"]
+  insert_commute [of "Crypt X K" "Nonce N"]
+  insert_commute [of "Crypt X K" "Number N"]
+  insert_commute [of "Crypt X K" "Hash X'"]
+  insert_commute [of "Crypt X K" "MPair X' Y"]
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered. *}