# HG changeset patch
# User haftmann
# Date 1411311366 -7200
# Node ID 24096e89c131649e54003d97f80ed0e897f7321b
# Parent  bd5e49fca1fdb18c743fd465207a51d2a9aa6794
corrected slip in documentation

diff -r bd5e49fca1fd -r 24096e89c131 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.
 *}