--- a/ProgTutorial/Package/Ind_Code.thy	Sun Oct 11 01:47:15 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Oct 11 16:30:59 2009 +0200
@@ -37,7 +37,8 @@
   It returns the definition (as a theorem) and the local theory in which the
   definition has been made. In Line 4, @{ML_ind  internalK in Thm} is a flag
   attached to the theorem (other possibile flags are @{ML_ind  definitionK in Thm}
-  and @{ML_ind  axiomK in Thm}). These flags just classify theorems and have no
+  and @{ML_ind  axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.} 
+  These flags just classify theorems and have no
   significant meaning, except for tools that, for example, find theorems in
   the theorem database.\footnote{FIXME: put in the section about theorems.} We
   also use @{ML_ind  empty_binding in Attrib} in Line 3, since the definitions for