--- a/ProgTutorial/Tactical.thy	Tue Apr 07 17:04:39 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Apr 07 23:59:39 2009 +0100
@@ -1484,7 +1484,7 @@
 text {*
   where the second argument specifies the pattern and the right-hand side
   contains the code of the simproc (we have to use @{ML K} since we ignoring
-  an argument about morphisms\footnote{FIXME: what does the morphism do?}). 
+  an argument about morphisms. 
   After this, the simplifier is aware of the simproc and you can test whether 
   it fires on the lemma:
 *}