diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/Appendix.thy	Wed Oct 26 12:59:44 2011 +0100
@@ -21,7 +21,7 @@
 
   \begin{itemize}
   \item translations/print translations; 
-  @{ML "ProofContext.print_syntax"}
+  @{ML "Proof_Context.print_syntax"}
   
   \item user space type systems (in the form that already exists)