--- a/ProgTutorial/FirstSteps.thy Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Oct 18 21:22:44 2009 +0200
@@ -822,8 +822,8 @@
@{ML_file "Pure/General/binding.ML"}.
\end{readmore}
- \footnote{\bf FIXME give a better example why bindings are important; maybe
- give a pointer to \isacommand{local\_setup}; if not, then explain
+ \footnote{\bf FIXME give a better example why bindings are important}
+ \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
why @{ML snd} is needed.}
\footnote{\bf FIXME: There should probably a separate section on binding, long-names
and sign.}