
diff -r 10a9c31a22b4 -r 50fca9d09528 doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Feb 15 13:24:22 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Feb 15 17:49:03 2012 +0100
@@ -10,7 +10,7 @@
   additional means for reading and printing of terms and types.  This
   important add-on outside the logical core is called \emph{inner
   syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of
-  the theory and proof language (cf.\ \chref{FIXME}).
+  the theory and proof language (cf.\ \cite{isabelle-isar-ref}).
 
   For example, according to \cite{church40} quantifiers are
   represented as higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow>




