# HG changeset patch
# User wenzelm
# Date 1322738727 -3600
# Node ID c7a13ce601613a1c098739469e1b165d3d67ae6c
# Parent  7df60d1aa988801084d959e1dddf65a9f1edca9f
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

diff -r 7df60d1aa988 -r c7a13ce60161 NEWS
--- a/NEWS	Thu Dec 01 11:54:39 2011 +0100
+++ b/NEWS	Thu Dec 01 12:25:27 2011 +0100
@@ -23,6 +23,11 @@
 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
 indices of schematic variables.
 
+* Renamed inner syntax categories "num" to "num_token" and "xnum" to
+"xnum_token", in accordance to existing "float_token".  Minor
+INCOMPATIBILITY.  Note that in practice "num_const" etc. are mainly
+used instead.
+
 
 *** Pure ***
 
diff -r 7df60d1aa988 -r c7a13ce60161 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 01 11:54:39 2011 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 01 12:25:27 2011 +0100
@@ -693,24 +693,24 @@
     @{syntax_def (inner) var} & = & @{syntax_ref var} \\
     @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
-    @{syntax_def (inner) num} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
+    @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
-    @{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
+    @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
 
     @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
   \end{supertabular}
   \end{center}
 
-  The token categories @{syntax (inner) num}, @{syntax (inner)
-  float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are
-  not used in Pure.  Object-logics may implement numerals and string
-  constants by adding appropriate syntax declarations, together with
-  some translation functions (e.g.\ see Isabelle/HOL).
+  The token categories @{syntax (inner) num_token}, @{syntax (inner)
+  float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
+  xstr} are not used in Pure.  Object-logics may implement numerals
+  and string constants by adding appropriate syntax declarations,
+  together with some translation functions (e.g.\ see Isabelle/HOL).
 
-  The derived categories @{syntax_def (inner) num_const} and
-  @{syntax_def (inner) float_const} provide robust access to @{syntax
-  (inner) num}, and @{syntax (inner) float_token}, respectively: the
-  syntax tree holds a syntactic constant instead of a free variable.
+  The derived categories @{syntax_def (inner) num_const}, @{syntax_def
+  (inner) float_const}, and @{syntax_def (inner) num_const} provide
+  robust access to the respective tokens: the syntax tree holds a
+  syntactic constant instead of a free variable.
 *}
 
 
diff -r 7df60d1aa988 -r c7a13ce60161 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 01 11:54:39 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 01 12:25:27 2011 +0100
@@ -866,22 +866,21 @@
     \indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\
     \indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\
     \indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\
-    \indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
+    \indexdef{inner}{syntax}{num\_token}\hypertarget{syntax.inner.num-token}{\hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
     \indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
-    \indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
+    \indexdef{inner}{syntax}{xnum\_token}\hypertarget{syntax.inner.xnum-token}{\hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
 
     \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|''| \\
   \end{supertabular}
   \end{center}
 
-  The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are
-  not used in Pure.  Object-logics may implement numerals and string
-  constants by adding appropriate syntax declarations, together with
-  some translation functions (e.g.\ see Isabelle/HOL).
+  The token categories \hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are not used in Pure.  Object-logics may implement numerals
+  and string constants by adding appropriate syntax declarations,
+  together with some translation functions (e.g.\ see Isabelle/HOL).
 
-  The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}} and
-  \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, respectively: the
-  syntax tree holds a syntactic constant instead of a free variable.%
+  The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}}, \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}const}}}}, and \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}} provide
+  robust access to the respective tokens: the syntax tree holds a
+  syntactic constant instead of a free variable.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 7df60d1aa988 -r c7a13ce60161 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Dec 01 11:54:39 2011 +0100
+++ b/src/HOL/ex/Numeral.thy	Thu Dec 01 12:25:27 2011 +0100
@@ -274,7 +274,7 @@
 *}
 
 syntax
-  "_Numerals" :: "xnum \<Rightarrow> 'a"    ("_")
+  "_Numerals" :: "xnum_token \<Rightarrow> 'a"    ("_")
 
 parse_translation {*
 let
diff -r 7df60d1aa988 -r c7a13ce60161 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Dec 01 12:25:27 2011 +0100
@@ -177,9 +177,9 @@
   ("var", VarSy),
   ("tid", TFreeSy),
   ("tvar", TVarSy),
-  ("num", NumSy),
+  ("num_token", NumSy),
   ("float_token", FloatSy),
-  ("xnum", XNumSy),
+  ("xnum_token", XNumSy),
   ("xstr", StrSy)];
 
 val terminals = map #1 terminal_kinds;
diff -r 7df60d1aa988 -r c7a13ce60161 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Dec 01 12:25:27 2011 +0100
@@ -547,7 +547,7 @@
 val basic_nonterms =
   (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
-    "any", "prop'", "num_const", "float_const", "index", "struct",
+    "any", "prop'", "num_const", "float_const", "xnum_const", "index", "struct",
     "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
 
 
diff -r 7df60d1aa988 -r c7a13ce60161 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/pure_thy.ML	Thu Dec 01 12:25:27 2011 +0100
@@ -125,8 +125,9 @@
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_strip_positions", typ "'a", NoSyn),
-    ("_constify",   typ "num => num_const",            Delimfix "_"),
+    ("_constify",   typ "num_token => num_const",      Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
+    ("_constify",   typ "xnum_token => xnum_const",    Delimfix "_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
@@ -135,7 +136,7 @@
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position",   typ "id => id_position",           Delimfix "_"),
     ("_position",   typ "longid => longid_position",   Delimfix "_"),
-    ("_position",   typ "xstr => xstr_position",   Delimfix "_"),
+    ("_position",   typ "xstr => xstr_position",       Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
     ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
     ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
diff -r 7df60d1aa988 -r c7a13ce60161 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Thu Dec 01 11:54:39 2011 +0100
+++ b/src/ZF/Bin.thy	Thu Dec 01 12:25:27 2011 +0100
@@ -102,7 +102,7 @@
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int"    :: "xnum => i"        ("_")
+  "_Int"    :: "xnum_token => i"        ("_")
 
 use "Tools/numeral_syntax.ML"
 setup Numeral_Syntax.setup