doc-src/IsarImplementation/Thy/Prelim.thy

   end-users using existing notation for attributes (cf.\
   \secref{sec:attributes}).
 
   For example, the predefined configuration option @{attribute
   show_types} controls output of explicit type constraints for
-  variables in printed terms (cf.\ \secref{sec:parse-print}).  Its
+  variables in printed terms (cf.\ \secref{sec:read-print}).  Its
   value can be modified within Isar text like this:
 *}
 
 declare [[show_types = false]]
   -- {* declaration within (local) theory context *}