--- a/ProgTutorial/General.thy	Fri Oct 30 09:42:17 2009 +0100
+++ b/ProgTutorial/General.thy	Sat Oct 31 11:37:41 2009 +0100
@@ -1366,7 +1366,7 @@
 text {*
   This gives a function from @{ML_type "theory -> theory"}, which
   can be used for example with \isacommand{setup} or with
-  @{ML "Context.>> o Context.map_theory"}.
+  @{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.}
 
   As an example of a slightly more complicated theorem attribute, we implement 
   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
@@ -1375,7 +1375,8 @@
 *}
 
 ML{*fun MY_THEN thms = 
-  Thm.rule_attribute (fn _ => fn thm => List.foldl ((op RS) o swap) thm thms)*}
+  Thm.rule_attribute 
+    (fn _ => fn thm => fold (curry ((op RS) o swap)) thms thm)*}
 
 text {* 
   where @{ML swap} swaps the components of a pair. The setup of this theorem