diff -r 364fffa80794 -r f118240ab44a ProgTutorial/FirstSteps.thy --- 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.}