diff -r ea71549629e2 -r 0dff3326d12a src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/System/Basics.thy	Mon Dec 09 20:16:12 2013 +0100
@@ -95,7 +95,7 @@
   of these may have to be adapted (probably @{setting ML_SYSTEM}
   etc.).
   
-  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
+  \item The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
   exists) is run in the same way as the site default settings. Note
   that the variable @{setting ISABELLE_HOME_USER} has already been set
   before --- usually to something like @{verbatim
@@ -166,7 +166,7 @@
   
   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   counterpart of @{setting ISABELLE_HOME}. The default value is
-  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
+  relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
   circumstances this may be changed in the global setting file.
   Typically, the @{setting ISABELLE_HOME_USER} directory mimics
   @{setting ISABELLE_HOME} to some extend. In particular, site-wide
@@ -247,7 +247,7 @@
   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
   theory browser information (HTML text, graph data, and printable
   documents) is stored (see also \secref{sec:info}).  The default
-  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
+  value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
   
   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
   load if none is given explicitely by the user.  The default value is
@@ -277,7 +277,7 @@
   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   prefix from which any running @{executable "isabelle-process"}
   derives an individual directory for temporary files.  The default is
-  somewhere in @{verbatim "/tmp"}.
+  somewhere in @{file_unchecked "/tmp"}.
   
   \end{description}
 *}
@@ -325,7 +325,7 @@
   itself.  After initializing all of its sub-components recursively,
   @{setting ISABELLE_HOME_USER} is included in the same manner (if
   that directory exists).  This allows to install private components
-  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+  via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
   often more convenient to do that programmatically via the
   \verb,init_component, shell function in the \verb,etc/settings,
   script of \verb,$ISABELLE_HOME_USER, (or any other component