--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Sep 20 10:44:24 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Sep 21 16:56:06 2014 +0200
@@ -617,7 +617,7 @@
@{file "~~/src/HOL/Tools/string_syntax.ML"}).
The derived categories @{syntax_def (inner) num_const}, @{syntax_def
- (inner) float_const}, and @{syntax_def (inner) num_const} provide
+ (inner) float_const}, and @{syntax_def (inner) xnum_const} provide
robust access to the respective tokens: the syntax tree holds a
syntactic constant instead of a free variable.
*}