--- a/ProgTutorial/Essential.thy	Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Essential.thy	Tue Dec 01 12:25:34 2009 +0100
@@ -1685,7 +1685,7 @@
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
   in the structure @{ML_struct Goal}. For example below we use this function
-  to prove the term @{term "P \<Longrightarrow> P"}.
+  to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?}
   
   @{ML_response_fake [display,gray]
   "let