diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -566,7 +566,7 @@
 subsection {* A basic fold functional for finite sets *}
 
 text {* The intended behaviour is
-@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
+@{text "fold f z {x\<^sub>1, ..., x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)"}
 if @{text f} is ``left-commutative'':
 *}