diff -r 310e9b810bbf -r a10fc2bd3182 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 04 20:11:19 2012 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 04 20:12:01 2012 +0100
@@ -11,7 +11,7 @@
   for the parser and output templates for the pretty printer.
 
   In full generality, parser and pretty printer configuration is a
-  subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
+  subtle affair~\cite{isabelle-isar-ref}.  Your syntax specifications need
   to interact properly with the existing setup of Isabelle/Pure and
   Isabelle/HOL\@.  To avoid creating ambiguities with existing
   elements, it is particularly important to give new syntactic
@@ -154,7 +154,7 @@
   be displayed after further input.
 
   More flexible is to provide alternative syntax forms
-  through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
+  through the \bfindex{print mode} concept~\cite{isabelle-isar-ref}.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of @{text xor}:
@@ -188,7 +188,7 @@
 
 text {*
   Prefix syntax annotations\index{prefix annotation} are another form
-  of mixfixes \cite{isabelle-ref}, without any template arguments or
+  of mixfixes \cite{isabelle-isar-ref}, without any template arguments or
   priorities --- just some literal syntax.  The following example
   associates common symbols with the constructors of a datatype.
 *}
@@ -263,7 +263,7 @@
 
 Abbreviations are a simplified form of the general concept of
 \emph{syntax translations}; even heavier transformations may be
-written in ML \cite{isabelle-ref}.
+written in ML \cite{isabelle-isar-ref}.
 *}
 
 
@@ -531,7 +531,7 @@
   theory or proof context (\bfindex{text blocks}).
 
   \medskip Marginal comments are part of each command's concrete
-  syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
+  syntax \cite{isabelle-isar-ref}; the common form is ``\verb,--,~$text$''
   where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
   marginal comments may be given at the same time.  Here is a simple