diff -r d43f46423298 -r baa2970a9687 Paper.thy
--- a/Paper.thy	Fri Sep 06 13:27:46 2013 +0100
+++ b/Paper.thy	Fri Sep 06 14:55:53 2013 +0100
@@ -956,7 +956,7 @@
   
   \noindent
   generating an optional value.
-  The first clause states that the anchor of the @{text
+  The first clause states that the @{text
   root}-directory is always its own anchor unless it has been
   deleted. If a file is present in the initial state and not deleted
   in @{text s}, then it is also its own anchor, otherwise the anchor