--- a/src/Doc/IsarRef/Inner_Syntax.thy Sat Dec 29 17:18:01 2012 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Sat Dec 29 23:15:51 2012 +0100
@@ -353,7 +353,7 @@
Isabelle types and terms. Locally fixed parameters in toplevel
theorem statements, locale and class specifications also admit
mixfix annotations in a fairly uniform manner. A mixfix annotation
- describes describes the concrete syntax, the translation to abstract
+ describes the concrete syntax, the translation to abstract
syntax, and the pretty printing. Special case annotations provide a
simple means of specifying infix operators and binders.