diff -r 56b6cdce22f1 -r 026f3db3f5c6 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -789,7 +789,7 @@
     be pulled out using the @{text analz_insert} rules*}
 ML
 {*
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
+fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
 bind_thms ("pushKeys",
            map (insComm "Key ?K")