diff -r fb94df4505a0 -r 703ea96b13c6 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sun Mar 13 20:21:24 2011 +0100
+++ b/doc-src/System/Thy/document/Basics.tex	Sun Mar 13 20:56:00 2011 +0100
@@ -236,13 +236,6 @@
   typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
   \verb|IsaMakefile|s in the distribution).
 
-  \item[\indexdef{}{setting}{ISABELLE\_FILE\_IDENT}\hypertarget{setting.ISABELLE-FILE-IDENT}{\hyperlink{setting.ISABELLE-FILE-IDENT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}FILE{\isaliteral{5F}{\isacharunderscore}}IDENT}}}}}] specifies a shell command
-  for producing a source file identification, based on the actual
-  content instead of the full physical path and date stamp (which is
-  the default). A typical identification would produce a ``digest'' of
-  the text, using a cryptographic hash function like SHA-1, for
-  example.
-  
   \item[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle
   document preparation (see also \secref{sec:tool-latex}).