--- a/ProgTutorial/Tactical.thy	Tue Oct 06 11:35:00 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Oct 06 16:40:37 2009 +0200
@@ -1122,6 +1122,8 @@
   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 
   \end{exercise}
 
+  \footnote{\bf FIXME: explain @{ML_ind Cong_Tac.cong_tac}}
+
 *}
 
 section {* Simplifier Tactics *}