--- a/ProgTutorial/Solutions.thy	Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Thu Aug 20 22:30:20 2009 +0200
@@ -11,7 +11,7 @@
   | rev_sum t = t *}
 
 text {* 
-  An alternative solution using the function @{ML [index] mk_binop in HOLogic} is:
+  An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
  *}
 
 ML{*fun rev_sum t =