eliminated "xname" and variants;
authorwenzelm
Wed Apr 13 18:01:05 2016 +0200 (2016-04-13 ago)
changeset 629699f394a16c557
parent 62968 4e4738698db4
child 62970 f78cf782bd33
eliminated "xname" and variants;
NEWS
src/Doc/Datatypes/Datatypes.thy
src/Doc/Eisbach/Manual.thy
src/Doc/Implementation/Isar.thy
src/Doc/Implementation/Logic.thy
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Prelim.thy
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Proof_Script.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/JEdit/JEdit.thy
src/Doc/Logics_ZF/ZF_Isar.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Library/rewrite.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/SPARK/Manual/Reference.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/BNF/bnf_lift.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/HOL/Tools/try0.ML
src/HOL/Tools/value.ML
src/Pure/General/completion.scala
src/Pure/Isar/method.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse.scala
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/ML/ml_context.ML
src/Pure/PIDE/command.scala
src/Pure/Pure.thy
src/Pure/Thy/sessions.scala
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Tools/Code/code_target.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/NEWS	Wed Apr 13 17:00:02 2016 +0200
     1.2 +++ b/NEWS	Wed Apr 13 18:01:05 2016 +0200
     1.3 @@ -16,6 +16,10 @@
     1.4  INCOMPATIBILITY, need to provide explicit type constraints for Pure
     1.5  types where this is really intended.
     1.6  
     1.7 +* Simplified outer syntax: uniform category "name" includes long
     1.8 +identifiers. Former "xname" / "nameref" / "name reference" has been
     1.9 +discontinued.
    1.10 +
    1.11  * Mixfix annotations support general block properties, with syntax
    1.12  "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
    1.13  "unbreakable", "markup". The existing notation "(DIGITS" is equivalent
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 13 17:00:02 2016 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 13 18:01:05 2016 +0200
     2.3 @@ -3020,7 +3020,7 @@
     2.4  @{rail \<open>
     2.5    @@{command lift_bnf} target? lb_options? \<newline>
     2.6      @{syntax tyargs} name wit_terms?  \<newline>
     2.7 -    ('via' thmref)? @{syntax map_rel}?
     2.8 +    ('via' thm)? @{syntax map_rel}?
     2.9    ;
    2.10    @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
    2.11    ;
    2.12 @@ -3055,7 +3055,7 @@
    2.13  
    2.14  @{rail \<open>
    2.15    @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
    2.16 -    @{syntax tyargs} name ('via' thmref)? @{syntax map_rel}?
    2.17 +    @{syntax tyargs} name ('via' thm)? @{syntax map_rel}?
    2.18  \<close>}
    2.19  \medskip
    2.20  
    2.21 @@ -3203,7 +3203,7 @@
    2.22  
    2.23  @{rail \<open>
    2.24    @@{command simps_of_case} target? (name ':')? \<newline>
    2.25 -    (thmref + ) (@'splits' ':' (thmref + ))?
    2.26 +    (thm + ) (@'splits' ':' (thm + ))?
    2.27  \<close>}
    2.28  
    2.29  \medskip
    2.30 @@ -3242,7 +3242,7 @@
    2.31  
    2.32  @{rail \<open>
    2.33    @@{command case_of_simps} target? (name ':')? \<newline>
    2.34 -    (thmref + )
    2.35 +    (thm + )
    2.36  \<close>}
    2.37  
    2.38  \medskip
     3.1 --- a/src/Doc/Eisbach/Manual.thy	Wed Apr 13 17:00:02 2016 +0200
     3.2 +++ b/src/Doc/Eisbach/Manual.thy	Wed Apr 13 18:01:05 2016 +0200
     3.3 @@ -288,7 +288,7 @@
     3.4      ;
     3.5      kind:
     3.6        (@'conclusion' | @'premises' ('(' 'local' ')')? |
     3.7 -       '(' term ')' | @{syntax thmrefs})
     3.8 +       '(' term ')' | @{syntax thms})
     3.9      ;
    3.10      pattern: fact_name? term args? \<newline> (@'for' fixes)?
    3.11      ;
     4.1 --- a/src/Doc/Implementation/Isar.thy	Wed Apr 13 17:00:02 2016 +0200
     4.2 +++ b/src/Doc/Implementation/Isar.thy	Wed Apr 13 18:01:05 2016 +0200
     4.3 @@ -363,7 +363,7 @@
     4.4  
     4.5    The @{ML Attrib.thms} parser produces a list of theorems from the usual Isar
     4.6    syntax involving attribute expressions etc.\ (syntax category @{syntax
     4.7 -  thmrefs}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
     4.8 +  thms}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
     4.9    added to @{ML HOL_basic_ss} which already contains the basic Simplifier
    4.10    setup for HOL.
    4.11  
     5.1 --- a/src/Doc/Implementation/Logic.thy	Wed Apr 13 17:00:02 2016 +0200
     5.2 +++ b/src/Doc/Implementation/Logic.thy	Wed Apr 13 18:01:05 2016 +0200
     5.3 @@ -171,13 +171,13 @@
     5.4    \end{matharray}
     5.5  
     5.6    @{rail \<open>
     5.7 -  @@{ML_antiquotation class} nameref
     5.8 +  @@{ML_antiquotation class} name
     5.9    ;
    5.10    @@{ML_antiquotation sort} sort
    5.11    ;
    5.12    (@@{ML_antiquotation type_name} |
    5.13     @@{ML_antiquotation type_abbrev} |
    5.14 -   @@{ML_antiquotation nonterminal}) nameref
    5.15 +   @@{ML_antiquotation nonterminal}) name
    5.16    ;
    5.17    @@{ML_antiquotation typ} type
    5.18    \<close>}
    5.19 @@ -392,7 +392,7 @@
    5.20  
    5.21    @{rail \<open>
    5.22    (@@{ML_antiquotation const_name} |
    5.23 -   @@{ML_antiquotation const_abbrev}) nameref
    5.24 +   @@{ML_antiquotation const_abbrev}) name
    5.25    ;
    5.26    @@{ML_antiquotation const} ('(' (type + ',') ')')?
    5.27    ;
    5.28 @@ -701,9 +701,9 @@
    5.29    ;
    5.30    @@{ML_antiquotation cprop} prop
    5.31    ;
    5.32 -  @@{ML_antiquotation thm} thmref
    5.33 +  @@{ML_antiquotation thm} thm
    5.34    ;
    5.35 -  @@{ML_antiquotation thms} thmrefs
    5.36 +  @@{ML_antiquotation thms} thms
    5.37    ;
    5.38    @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
    5.39      @'by' method method?
     6.1 --- a/src/Doc/Implementation/ML.thy	Wed Apr 13 17:00:02 2016 +0200
     6.2 +++ b/src/Doc/Implementation/ML.thy	Wed Apr 13 18:01:05 2016 +0200
     6.3 @@ -653,10 +653,10 @@
     6.4    special syntactic entities of the following form:
     6.5  
     6.6    @{rail \<open>
     6.7 -  @{syntax_def antiquote}: '@{' nameref args '}'
     6.8 +  @{syntax_def antiquote}: '@{' name args '}'
     6.9    \<close>}
    6.10  
    6.11 -  Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
    6.12 +  Here @{syntax name} and @{syntax args} are outer syntax categories, as
    6.13    defined in @{cite "isabelle-isar-ref"}.
    6.14  
    6.15    \<^medskip>
     7.1 --- a/src/Doc/Implementation/Prelim.thy	Wed Apr 13 17:00:02 2016 +0200
     7.2 +++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 13 18:01:05 2016 +0200
     7.3 @@ -142,9 +142,9 @@
     7.4    \end{matharray}
     7.5  
     7.6    @{rail \<open>
     7.7 -  @@{ML_antiquotation theory} nameref?
     7.8 +  @@{ML_antiquotation theory} name?
     7.9    ;
    7.10 -  @@{ML_antiquotation theory_context} nameref
    7.11 +  @@{ML_antiquotation theory_context} name
    7.12    \<close>}
    7.13  
    7.14    \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
     8.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 17:00:02 2016 +0200
     8.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 18:01:05 2016 +0200
     8.3 @@ -167,7 +167,7 @@
     8.4        (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
     8.5          options @{syntax text} |
     8.6        @@{antiquotation theory} options @{syntax name} |
     8.7 -      @@{antiquotation thm} options styles @{syntax thmrefs} |
     8.8 +      @@{antiquotation thm} options styles @{syntax thms} |
     8.9        @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
    8.10        @@{antiquotation prop} options styles @{syntax prop} |
    8.11        @@{antiquotation term} options styles @{syntax term} |
    8.12 @@ -185,8 +185,8 @@
    8.13      @{syntax antiquotation}:
    8.14        @@{antiquotation goals} options |
    8.15        @@{antiquotation subgoals} options |
    8.16 -      @@{antiquotation prf} options @{syntax thmrefs} |
    8.17 -      @@{antiquotation full_prf} options @{syntax thmrefs} |
    8.18 +      @@{antiquotation prf} options @{syntax thms} |
    8.19 +      @@{antiquotation full_prf} options @{syntax thms} |
    8.20        @@{antiquotation ML} options @{syntax text} |
    8.21        @@{antiquotation ML_op} options @{syntax text} |
    8.22        @@{antiquotation ML_type} options @{syntax text} |
    8.23 @@ -195,8 +195,8 @@
    8.24        @@{antiquotation emph} options @{syntax text} |
    8.25        @@{antiquotation bold} options @{syntax text} |
    8.26        @@{antiquotation verbatim} options @{syntax text} |
    8.27 -      @@{antiquotation "file"} options @{syntax xname} |
    8.28 -      @@{antiquotation file_unchecked} options @{syntax xname} |
    8.29 +      @@{antiquotation "file"} options @{syntax name} |
    8.30 +      @@{antiquotation file_unchecked} options @{syntax name} |
    8.31        @@{antiquotation url} options @{syntax name} |
    8.32        @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
    8.33      ;
    8.34 @@ -613,7 +613,7 @@
    8.35    \end{matharray}
    8.36  
    8.37    @{rail \<open>
    8.38 -    @@{command display_drafts} (@{syntax xname} +)
    8.39 +    @@{command display_drafts} (@{syntax name} +)
    8.40    \<close>}
    8.41  
    8.42    \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
     9.1 --- a/src/Doc/Isar_Ref/Generic.thy	Wed Apr 13 17:00:02 2016 +0200
     9.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Wed Apr 13 18:01:05 2016 +0200
     9.3 @@ -71,12 +71,12 @@
     9.4    \end{matharray}
     9.5  
     9.6    @{rail \<open>
     9.7 -    (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
     9.8 +    (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thms}
     9.9      ;
    9.10      (@@{method erule} | @@{method drule} | @@{method frule})
    9.11 -      ('(' @{syntax nat} ')')? @{syntax thmrefs}
    9.12 +      ('(' @{syntax nat} ')')? @{syntax thms}
    9.13      ;
    9.14 -    (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
    9.15 +    (@@{method intro} | @@{method elim}) @{syntax thms}?
    9.16      ;
    9.17      @@{method sleep} @{syntax real}
    9.18    \<close>}
    9.19 @@ -140,9 +140,9 @@
    9.20      ;
    9.21      @@{attribute untagged} @{syntax name}
    9.22      ;
    9.23 -    @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
    9.24 +    @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thm}
    9.25      ;
    9.26 -    (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
    9.27 +    (@@{attribute unfolded} | @@{attribute folded}) @{syntax thms}
    9.28      ;
    9.29      @@{attribute rotated} @{syntax int}?
    9.30    \<close>}
    9.31 @@ -192,9 +192,9 @@
    9.32    \end{matharray}
    9.33  
    9.34    @{rail \<open>
    9.35 -    @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
    9.36 +    @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thm}
    9.37      ;
    9.38 -    @@{method split} @{syntax thmrefs}
    9.39 +    @@{method split} @{syntax thms}
    9.40    \<close>}
    9.41  
    9.42    These methods provide low-level facilities for equational reasoning
    9.43 @@ -284,7 +284,7 @@
    9.44      opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
    9.45      ;
    9.46      @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
    9.47 -      'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
    9.48 +      'cong' (() | 'add' | 'del')) ':' @{syntax thms}
    9.49    \<close>}
    9.50  
    9.51    \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
    9.52 @@ -1063,7 +1063,7 @@
    9.53    \end{matharray}
    9.54  
    9.55    @{rail \<open>
    9.56 -    @@{attribute simplified} opt? @{syntax thmrefs}?
    9.57 +    @@{attribute simplified} opt? @{syntax thms}?
    9.58      ;
    9.59  
    9.60      opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
    9.61 @@ -1383,7 +1383,7 @@
    9.62    \end{matharray}
    9.63  
    9.64    @{rail \<open>
    9.65 -    @@{method rule} @{syntax thmrefs}?
    9.66 +    @@{method rule} @{syntax thms}?
    9.67    \<close>}
    9.68  
    9.69    \<^descr> @{method rule} as offered by the Classical Reasoner is a
    9.70 @@ -1434,12 +1434,12 @@
    9.71      @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
    9.72      ;
    9.73      @{syntax_def clamod}:
    9.74 -      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
    9.75 +      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thms}
    9.76      ;
    9.77      @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
    9.78        ('cong' | 'split') (() | 'add' | 'del') |
    9.79        'iff' (((() | 'add') '?'?) | 'del') |
    9.80 -      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
    9.81 +      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thms}
    9.82    \<close>}
    9.83  
    9.84    \<^descr> @{method blast} is a separate classical tableau prover that
    10.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 13 17:00:02 2016 +0200
    10.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 13 18:01:05 2016 +0200
    10.3 @@ -109,7 +109,7 @@
    10.4      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
    10.5        @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
    10.6        @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
    10.7 -      (@'where' clauses)? (@'monos' @{syntax thmrefs})?
    10.8 +      (@'where' clauses)? (@'monos' @{syntax thms})?
    10.9      ;
   10.10      clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
   10.11      ;
   10.12 @@ -568,7 +568,7 @@
   10.13    \end{matharray}
   10.14  
   10.15    @{rail \<open>
   10.16 -    @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
   10.17 +    @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
   10.18        @'where' @{syntax thmdecl}? @{syntax prop}
   10.19    \<close>}
   10.20  
   10.21 @@ -638,7 +638,7 @@
   10.22      hints: '(' @'hints' ( recdefmod * ) ')'
   10.23      ;
   10.24      recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
   10.25 -      (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
   10.26 +      (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
   10.27    \<close>}
   10.28  
   10.29    \<^descr> @{command (HOL) "recdef"} defines general well-founded
   10.30 @@ -689,7 +689,7 @@
   10.31  
   10.32    @{rail \<open>
   10.33      (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
   10.34 -      (@{syntax nameref} (@{syntax term} + ) + @'and')
   10.35 +      (@{syntax name} (@{syntax term} + ) + @'and')
   10.36    \<close>}
   10.37  
   10.38    \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close>
   10.39 @@ -1265,7 +1265,7 @@
   10.40      ;
   10.41      quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
   10.42      ;
   10.43 -    quot_parametric: @'parametric' @{syntax thmref}
   10.44 +    quot_parametric: @'parametric' @{syntax thm}
   10.45    \<close>}
   10.46  
   10.47    \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL)
   10.48 @@ -1321,19 +1321,19 @@
   10.49    \end{matharray}
   10.50  
   10.51    @{rail \<open>
   10.52 -    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
   10.53 -      (@'parametric' @{syntax thmref})?
   10.54 +    @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? \<newline>
   10.55 +      (@'parametric' @{syntax thm})?
   10.56      ;
   10.57      @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
   10.58        @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
   10.59 -      (@'parametric' (@{syntax thmref}+))?
   10.60 +      (@'parametric' (@{syntax thm}+))?
   10.61      ;
   10.62 -    @@{command (HOL) lifting_forget} @{syntax nameref}
   10.63 +    @@{command (HOL) lifting_forget} @{syntax name}
   10.64      ;
   10.65 -    @@{command (HOL) lifting_update} @{syntax nameref}
   10.66 +    @@{command (HOL) lifting_update} @{syntax name}
   10.67      ;
   10.68      @@{attribute (HOL) lifting_restore}
   10.69 -      @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
   10.70 +      @{syntax thm} (@{syntax thm} @{syntax thm})?
   10.71    \<close>}
   10.72  
   10.73    \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
   10.74 @@ -1661,9 +1661,9 @@
   10.75      ;
   10.76      constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
   10.77      ;
   10.78 -    @@{method (HOL) lifting} @{syntax thmrefs}?
   10.79 +    @@{method (HOL) lifting} @{syntax thms}?
   10.80      ;
   10.81 -    @@{method (HOL) lifting_setup} @{syntax thmrefs}?
   10.82 +    @@{method (HOL) lifting_setup} @{syntax thms}?
   10.83    \<close>}
   10.84  
   10.85    \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the
   10.86 @@ -1750,7 +1750,7 @@
   10.87      @@{command (HOL) try}
   10.88      ;
   10.89  
   10.90 -    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
   10.91 +    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
   10.92        @{syntax nat}?
   10.93      ;
   10.94  
   10.95 @@ -1761,7 +1761,7 @@
   10.96      ;
   10.97      args: ( @{syntax name} '=' value + ',' )
   10.98      ;
   10.99 -    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
  10.100 +    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
  10.101    \<close>} % FIXME check args "value"
  10.102  
  10.103    \<^descr> @{command (HOL) "solve_direct"} checks whether the current
  10.104 @@ -1822,7 +1822,7 @@
  10.105        @@{command (HOL) nitpick_params}) ( '[' args ']' )?
  10.106      ;
  10.107  
  10.108 -    @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>
  10.109 +    @@{command (HOL) quickcheck_generator} @{syntax name} \<newline>
  10.110        'operations:' ( @{syntax term} +)
  10.111      ;
  10.112  
  10.113 @@ -2140,11 +2140,11 @@
  10.114    \end{matharray}
  10.115  
  10.116    @{rail \<open>
  10.117 -    @@{method (HOL) meson} @{syntax thmrefs}?
  10.118 +    @@{method (HOL) meson} @{syntax thms}?
  10.119      ;
  10.120      @@{method (HOL) metis}
  10.121        ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
  10.122 -      @{syntax thmrefs}?
  10.123 +      @{syntax thms}?
  10.124    \<close>}
  10.125  
  10.126    \<^descr> @{method (HOL) meson} implements Loveland's model elimination
  10.127 @@ -2170,8 +2170,8 @@
  10.128  
  10.129    @{rail \<open>
  10.130      @@{method (HOL) algebra}
  10.131 -      ('add' ':' @{syntax thmrefs})?
  10.132 -      ('del' ':' @{syntax thmrefs})?
  10.133 +      ('add' ':' @{syntax thms})?
  10.134 +      ('del' ':' @{syntax thms})?
  10.135      ;
  10.136      @@{attribute (HOL) algebra} (() | 'add' | 'del')
  10.137    \<close>}
  10.138 @@ -2246,7 +2246,7 @@
  10.139    \end{matharray}
  10.140  
  10.141    @{rail \<open>
  10.142 -    @@{method (HOL) coherent} @{syntax thmrefs}?
  10.143 +    @@{method (HOL) coherent} @{syntax thms}?
  10.144    \<close>}
  10.145  
  10.146    \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent
  10.147 @@ -2279,7 +2279,7 @@
  10.148      ;
  10.149      @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
  10.150      ;
  10.151 -    rule: 'rule' ':' @{syntax thmref}
  10.152 +    rule: 'rule' ':' @{syntax thm}
  10.153    \<close>}
  10.154  
  10.155    \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
  10.156 @@ -2379,9 +2379,9 @@
  10.157      ;
  10.158      constexpr: ( const | 'name._' | '_' )
  10.159      ;
  10.160 -    typeconstructor: @{syntax nameref}
  10.161 +    typeconstructor: @{syntax name}
  10.162      ;
  10.163 -    class: @{syntax nameref}
  10.164 +    class: @{syntax name}
  10.165      ;
  10.166      target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
  10.167      ;
    11.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Apr 13 17:00:02 2016 +0200
    11.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Apr 13 18:01:05 2016 +0200
    11.3 @@ -53,9 +53,9 @@
    11.4      ;
    11.5      @@{command prop} @{syntax modes}? @{syntax prop}
    11.6      ;
    11.7 -    @@{command thm} @{syntax modes}? @{syntax thmrefs}
    11.8 +    @@{command thm} @{syntax modes}? @{syntax thms}
    11.9      ;
   11.10 -    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
   11.11 +    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thms}?
   11.12      ;
   11.13      @@{command print_state} @{syntax modes}?
   11.14      ;
   11.15 @@ -504,12 +504,12 @@
   11.16  
   11.17    @{rail \<open>
   11.18      (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
   11.19 -      (@{syntax nameref} @{syntax mixfix} + @'and')
   11.20 +      (@{syntax name} @{syntax mixfix} + @'and')
   11.21      ;
   11.22      (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
   11.23 -      (@{syntax nameref} @{syntax mixfix} + @'and')
   11.24 +      (@{syntax name} @{syntax mixfix} + @'and')
   11.25      ;
   11.26 -    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   11.27 +    @@{command write} @{syntax mode}? (@{syntax name} @{syntax mixfix} + @'and')
   11.28    \<close>}
   11.29  
   11.30    \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
   11.31 @@ -1103,7 +1103,7 @@
   11.32      ;
   11.33      mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
   11.34      ;
   11.35 -    transpat: ('(' @{syntax nameref} ')')? @{syntax string}
   11.36 +    transpat: ('(' @{syntax name} ')')? @{syntax string}
   11.37    \<close>}
   11.38  
   11.39    \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
    12.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 13 17:00:02 2016 +0200
    12.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 13 18:01:05 2016 +0200
    12.3 @@ -179,19 +179,14 @@
    12.4  
    12.5  text \<open>
    12.6    Entity @{syntax name} usually refers to any name of types, constants,
    12.7 -  theorems etc.\ that are to be \<^emph>\<open>declared\<close> or \<^emph>\<open>defined\<close> (so qualified
    12.8 -  identifiers are excluded here). Quoted strings provide an escape for
    12.9 -  non-identifier names or those ruled out by outer syntax keywords (e.g.\
   12.10 -  quoted \<^verbatim>\<open>"let"\<close>). Already existing objects are usually referenced by
   12.11 -  @{syntax nameref}.
   12.12 +  theorems etc.\ Quoted strings provide an escape for non-identifier names or
   12.13 +  those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
   12.14  
   12.15    @{rail \<open>
   12.16 -    @{syntax_def name}: @{syntax ident} | @{syntax symident} |
   12.17 -      @{syntax string} | @{syntax nat}
   12.18 +    @{syntax_def name}: @{syntax ident} | @{syntax longident} |
   12.19 +      @{syntax symident} | @{syntax string} | @{syntax nat}
   12.20      ;
   12.21      @{syntax_def par_name}: '(' @{syntax name} ')'
   12.22 -    ;
   12.23 -    @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   12.24    \<close>}
   12.25  \<close>
   12.26  
   12.27 @@ -219,13 +214,13 @@
   12.28  text \<open>
   12.29    Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
   12.30    i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
   12.31 -  convenience, any of the smaller text units conforming to @{syntax nameref}
   12.32 -  are admitted as well. A marginal @{syntax comment} is of the form
   12.33 -  \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
   12.34 -  within Isabelle/Isar commands.
   12.35 +  convenience, any of the smaller text units conforming to @{syntax name} are
   12.36 +  admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
   12.37 +  text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
   12.38 +  Isabelle/Isar commands.
   12.39  
   12.40    @{rail \<open>
   12.41 -    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
   12.42 +    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
   12.43      ;
   12.44      @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
   12.45    \<close>}
   12.46 @@ -241,9 +236,9 @@
   12.47    directly at the outer level.
   12.48  
   12.49    @{rail \<open>
   12.50 -    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
   12.51 +    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax name} + ','))?
   12.52      ;
   12.53 -    @{syntax_def sort}: @{syntax nameref}
   12.54 +    @{syntax_def sort}: @{syntax name}
   12.55      ;
   12.56      @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
   12.57    \<close>}
   12.58 @@ -265,10 +260,10 @@
   12.59    as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
   12.60  
   12.61    @{rail \<open>
   12.62 -    @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
   12.63 +    @{syntax_def type}: @{syntax name} | @{syntax typefree} |
   12.64        @{syntax typevar}
   12.65      ;
   12.66 -    @{syntax_def term}: @{syntax nameref} | @{syntax var}
   12.67 +    @{syntax_def term}: @{syntax name} | @{syntax var}
   12.68      ;
   12.69      @{syntax_def prop}: @{syntax term}
   12.70    \<close>}
   12.71 @@ -377,7 +372,7 @@
   12.72    conforming to @{syntax symident}.
   12.73  
   12.74    @{rail \<open>
   12.75 -    @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
   12.76 +    @{syntax_def atom}: @{syntax name} | @{syntax typefree} |
   12.77        @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
   12.78        @{syntax keyword} | @{syntax cartouche}
   12.79      ;
   12.80 @@ -385,13 +380,13 @@
   12.81      ;
   12.82      @{syntax_def args}: arg *
   12.83      ;
   12.84 -    @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
   12.85 +    @{syntax_def attributes}: '[' (@{syntax name} @{syntax args} * ',') ']'
   12.86    \<close>}
   12.87  
   12.88    Theorem specifications come in several flavors: @{syntax axmdecl} and
   12.89    @{syntax thmdecl} usually refer to axioms, assumptions or results of goal
   12.90    statements, while @{syntax thmdef} collects lists of existing theorems.
   12.91 -  Existing theorems are given by @{syntax thmref} and @{syntax thmrefs}, the
   12.92 +  Existing theorems are given by @{syntax thm} and @{syntax thms}, the
   12.93    former requires an actual singleton result.
   12.94  
   12.95    There are three forms of theorem references:
   12.96 @@ -426,12 +421,12 @@
   12.97      ;
   12.98      @{syntax_def thmdef}: thmbind '='
   12.99      ;
  12.100 -    @{syntax_def thmref}:
  12.101 -      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
  12.102 +    @{syntax_def thm}:
  12.103 +      (@{syntax name} selection? | @{syntax altstring} | @{syntax cartouche})
  12.104          @{syntax attributes}? |
  12.105        '[' @{syntax attributes} ']'
  12.106      ;
  12.107 -    @{syntax_def thmrefs}: @{syntax thmref} +
  12.108 +    @{syntax_def thms}: @{syntax thm} +
  12.109      ;
  12.110      selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
  12.111    \<close>}
  12.112 @@ -465,13 +460,13 @@
  12.113      ;
  12.114      @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
  12.115      ;
  12.116 -    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
  12.117 +    thm_criterion: ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
  12.118        'solves' | 'simp' ':' @{syntax term} | @{syntax term})
  12.119      ;
  12.120      @@{command find_consts} (const_criterion*)
  12.121      ;
  12.122      const_criterion: ('-'?)
  12.123 -      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
  12.124 +      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
  12.125      ;
  12.126      @@{command thm_deps} @{syntax thmrefs}
  12.127      ;
    13.1 --- a/src/Doc/Isar_Ref/Proof.thy	Wed Apr 13 17:00:02 2016 +0200
    13.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Wed Apr 13 18:01:05 2016 +0200
    13.3 @@ -283,10 +283,10 @@
    13.4    claim.
    13.5  
    13.6    @{rail \<open>
    13.7 -    @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    13.8 +    @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')
    13.9      ;
   13.10      (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
   13.11 -      (@{syntax thmrefs} + @'and')
   13.12 +      (@{syntax thms} + @'and')
   13.13    \<close>}
   13.14  
   13.15    \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
   13.16 @@ -386,7 +386,7 @@
   13.17      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
   13.18        stmt cond_stmt @{syntax for_fixes}
   13.19      ;
   13.20 -    @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
   13.21 +    @@{command print_statement} @{syntax modes}? @{syntax thms}
   13.22      ;
   13.23  
   13.24      stmt: (@{syntax props} + @'and')
   13.25 @@ -513,7 +513,7 @@
   13.26    \end{matharray}
   13.27  
   13.28    @{rail \<open>
   13.29 -    (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
   13.30 +    (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?
   13.31      ;
   13.32      @@{attribute trans} (() | 'add' | 'del')
   13.33    \<close>}
   13.34 @@ -571,16 +571,16 @@
   13.35    ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
   13.36    once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
   13.37    proof methods are usually just a comma separated list of @{syntax
   13.38 -  nameref}~@{syntax args} specifications. Note that parentheses may be dropped
   13.39 +  name}~@{syntax args} specifications. Note that parentheses may be dropped
   13.40    for single method specifications (with no arguments). The syntactic
   13.41    precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low
   13.42    to high).
   13.43  
   13.44    @{rail \<open>
   13.45      @{syntax_def method}:
   13.46 -      (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
   13.47 +      (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
   13.48      ;
   13.49 -    methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   13.50 +    methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   13.51    \<close>}
   13.52  
   13.53    Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
   13.54 @@ -753,19 +753,19 @@
   13.55    @{rail \<open>
   13.56      @@{method goal_cases} (@{syntax name}*)
   13.57      ;
   13.58 -    @@{method fact} @{syntax thmrefs}?
   13.59 +    @@{method fact} @{syntax thms}?
   13.60      ;
   13.61 -    @@{method (Pure) rule} @{syntax thmrefs}?
   13.62 +    @@{method (Pure) rule} @{syntax thms}?
   13.63      ;
   13.64      rulemod: ('intro' | 'elim' | 'dest')
   13.65 -      ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
   13.66 +      ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}
   13.67      ;
   13.68      (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
   13.69        ('!' | () | '?') @{syntax nat}?
   13.70      ;
   13.71      @@{attribute (Pure) rule} 'del'
   13.72      ;
   13.73 -    @@{attribute OF} @{syntax thmrefs}
   13.74 +    @@{attribute OF} @{syntax thms}
   13.75      ;
   13.76      @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
   13.77      ;
   13.78 @@ -968,7 +968,7 @@
   13.79    advanced case analysis later.
   13.80  
   13.81    @{rail \<open>
   13.82 -    @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
   13.83 +    @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')
   13.84      ;
   13.85      @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
   13.86      ;
   13.87 @@ -1076,7 +1076,7 @@
   13.88      @@{method coinduct} @{syntax insts} taking rule?
   13.89      ;
   13.90  
   13.91 -    rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
   13.92 +    rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)
   13.93      ;
   13.94      definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
   13.95      ;
   13.96 @@ -1253,7 +1253,7 @@
   13.97      @@{attribute coinduct} spec
   13.98      ;
   13.99  
  13.100 -    spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
  13.101 +    spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'
  13.102    \<close>}
  13.103  
  13.104    \<^descr> @{command "print_induct_rules"} prints cases and induct rules for
    14.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Wed Apr 13 17:00:02 2016 +0200
    14.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Wed Apr 13 18:01:05 2016 +0200
    14.3 @@ -37,7 +37,7 @@
    14.4    \end{matharray}
    14.5  
    14.6    @{rail \<open>
    14.7 -    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    14.8 +    @@{command supply} (@{syntax thmdef}? @{syntax thms} + @'and')
    14.9      ;
   14.10      ( @@{command apply} | @@{command apply_end} ) @{syntax method}
   14.11      ;
   14.12 @@ -222,7 +222,7 @@
   14.13    @{rail \<open>
   14.14      (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   14.15        @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
   14.16 -    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
   14.17 +    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thm} | @{syntax thms} )
   14.18      ;
   14.19      @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
   14.20      ;
    15.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 17:00:02 2016 +0200
    15.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 18:01:05 2016 +0200
    15.3 @@ -137,11 +137,11 @@
    15.4    \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.
    15.5  
    15.6    @{rail \<open>
    15.7 -    @@{command context} @{syntax nameref} @'begin'
    15.8 +    @@{command context} @{syntax name} @'begin'
    15.9      ;
   15.10      @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
   15.11      ;
   15.12 -    @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
   15.13 +    @{syntax_def target}: '(' @'in' @{syntax name} ')'
   15.14    \<close>}
   15.15  
   15.16    \<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing
   15.17 @@ -226,13 +226,13 @@
   15.18    (\secref{sec:locale}).
   15.19  
   15.20    @{rail \<open>
   15.21 -    @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
   15.22 +    @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
   15.23      ;
   15.24      @@{command print_bundles} ('!'?)
   15.25      ;
   15.26 -    (@@{command include} | @@{command including}) (@{syntax nameref}+)
   15.27 +    (@@{command include} | @@{command including}) (@{syntax name}+)
   15.28      ;
   15.29 -    @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
   15.30 +    @{syntax_def "includes"}: @'includes' (@{syntax name}+)
   15.31    \<close>}
   15.32  
   15.33    \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
   15.34 @@ -383,7 +383,7 @@
   15.35      (@@{command declaration} | @@{command syntax_declaration})
   15.36        ('(' @'pervasive' ')')? \<newline> @{syntax text}
   15.37      ;
   15.38 -    @@{command declare} (@{syntax thmrefs} + @'and')
   15.39 +    @@{command declare} (@{syntax thms} + @'and')
   15.40    \<close>}
   15.41  
   15.42    \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type @{ML_type
   15.43 @@ -440,7 +440,7 @@
   15.44    @{rail \<open>
   15.45      @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
   15.46      ;
   15.47 -    instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
   15.48 +    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
   15.49      ;
   15.50      qualifier: @{syntax name} ('?')?
   15.51      ;
   15.52 @@ -490,7 +490,7 @@
   15.53      ;
   15.54      @@{command experiment} (@{syntax context_elem}*) @'begin'
   15.55      ;
   15.56 -    @@{command print_locale} '!'? @{syntax nameref}
   15.57 +    @@{command print_locale} '!'? @{syntax name}
   15.58      ;
   15.59      @@{command print_locales} ('!'?)
   15.60      ;
   15.61 @@ -502,7 +502,7 @@
   15.62        @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
   15.63        @'assumes' (@{syntax props} + @'and') |
   15.64        @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
   15.65 -      @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   15.66 +      @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
   15.67    \<close>}
   15.68  
   15.69    \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
   15.70 @@ -628,12 +628,12 @@
   15.71      @@{command global_interpretation} @{syntax locale_expr} \<newline>
   15.72        definitions? equations?
   15.73      ;
   15.74 -    @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
   15.75 +    @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
   15.76        definitions? equations?
   15.77      ;
   15.78      @@{command print_dependencies} '!'? @{syntax locale_expr}
   15.79      ;
   15.80 -    @@{command print_interps} @{syntax nameref}
   15.81 +    @@{command print_interps} @{syntax name}
   15.82      ;
   15.83  
   15.84      definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
   15.85 @@ -798,15 +798,15 @@
   15.86      @@{command class} class_spec @'begin'?
   15.87      ;
   15.88      class_spec: @{syntax name} '='
   15.89 -      ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
   15.90 -        @{syntax nameref} | (@{syntax context_elem}+))      
   15.91 +      ((@{syntax name} '+' (@{syntax context_elem}+)) |
   15.92 +        @{syntax name} | (@{syntax context_elem}+))
   15.93      ;
   15.94 -    @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
   15.95 +    @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
   15.96      ;
   15.97 -    @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
   15.98 -      @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
   15.99 +    @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |
  15.100 +      @{syntax name} ('<' | '\<subseteq>') @{syntax name} )
  15.101      ;
  15.102 -    @@{command subclass} @{syntax nameref}
  15.103 +    @@{command subclass} @{syntax name}
  15.104      ;
  15.105      @@{command class_deps} (class_bounds class_bounds?)?
  15.106      ;
  15.107 @@ -1054,7 +1054,7 @@
  15.108        @@{command SML_file_no_debug} |
  15.109        @@{command ML_file} |
  15.110        @@{command ML_file_debug} |
  15.111 -      @@{command ML_file_no_debug}) @{syntax xname} ';'?
  15.112 +      @@{command ML_file_no_debug}) @{syntax name} ';'?
  15.113      ;
  15.114      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
  15.115        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
  15.116 @@ -1231,7 +1231,7 @@
  15.117    \end{matharray}
  15.118  
  15.119    @{rail \<open>
  15.120 -    @@{command lemmas} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
  15.121 +    @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')
  15.122        @{syntax for_fixes}
  15.123      ;
  15.124      @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
  15.125 @@ -1299,7 +1299,7 @@
  15.126  
  15.127    @{rail \<open>
  15.128      ( @{command hide_class} | @{command hide_type} |
  15.129 -      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
  15.130 +      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
  15.131    \<close>}
  15.132  
  15.133    Isabelle organizes any kind of name declarations (of types, constants,
    16.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Apr 13 17:00:02 2016 +0200
    16.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Apr 13 18:01:05 2016 +0200
    16.3 @@ -1068,7 +1068,7 @@
    16.4    single criterium has the following syntax:
    16.5  
    16.6    @{rail \<open>
    16.7 -    ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
    16.8 +    ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
    16.9        'solves' | 'simp' ':' @{syntax term} | @{syntax term})
   16.10    \<close>}
   16.11  
   16.12 @@ -1086,7 +1086,7 @@
   16.13  
   16.14    @{rail \<open>
   16.15      ('-'?)
   16.16 -      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
   16.17 +      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
   16.18    \<close>}
   16.19  
   16.20    See also the Isar command @{command_ref find_consts} in @{cite
    17.1 --- a/src/Doc/Logics_ZF/ZF_Isar.thy	Wed Apr 13 17:00:02 2016 +0200
    17.2 +++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Wed Apr 13 18:01:05 2016 +0200
    17.3 @@ -69,13 +69,13 @@
    17.4      hints: @{syntax (ZF) "monos"}? condefs? \<newline>
    17.5        @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
    17.6      ;
    17.7 -    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
    17.8 +    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thms}
    17.9      ;
   17.10 -    condefs: @'con_defs' @{syntax thmrefs}
   17.11 +    condefs: @'con_defs' @{syntax thms}
   17.12      ;
   17.13 -    @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
   17.14 +    @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thms}
   17.15      ;
   17.16 -    @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
   17.17 +    @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thms}
   17.18    \<close>}
   17.19  
   17.20    In the following syntax specification @{text "monos"}, @{text
    18.1 --- a/src/HOL/Decision_Procs/approximation.ML	Wed Apr 13 17:00:02 2016 +0200
    18.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Wed Apr 13 18:01:05 2016 +0200
    18.3 @@ -244,7 +244,7 @@
    18.4    end |> Pretty.writeln;
    18.5  
    18.6  val opt_modes =
    18.7 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    18.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
    18.9  
   18.10  val _ =
   18.11    Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
    19.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 13 17:00:02 2016 +0200
    19.2 +++ b/src/HOL/Library/rewrite.ML	Wed Apr 13 18:01:05 2016 +0200
    19.3 @@ -442,7 +442,7 @@
    19.4      val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
    19.5  
    19.6      val subst_parser =
    19.7 -      let val scan = raw_pattern -- to_parser -- Parse.xthms1
    19.8 +      let val scan = raw_pattern -- to_parser -- Parse.thms1
    19.9        in context_lift scan prep_args end
   19.10    in
   19.11      Method.setup @{binding rewrite} (subst_parser >>
    20.1 --- a/src/HOL/Library/simps_case_conv.ML	Wed Apr 13 17:00:02 2016 +0200
    20.2 +++ b/src/HOL/Library/simps_case_conv.ML	Wed Apr 13 18:01:05 2016 +0200
    20.3 @@ -231,15 +231,15 @@
    20.4  val _ =
    20.5    Outer_Syntax.local_theory @{command_keyword case_of_simps}
    20.6      "turn a list of equations into a case expression"
    20.7 -    (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
    20.8 +    (Parse_Spec.opt_thm_name ":"  -- Parse.thms1 >> case_of_simps_cmd)
    20.9  
   20.10  val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
   20.11 -  Parse.xthms1 --| @{keyword ")"}
   20.12 +  Parse.thms1 --| @{keyword ")"}
   20.13  
   20.14  val _ =
   20.15    Outer_Syntax.local_theory @{command_keyword simps_of_case}
   20.16      "perform case split on rule"
   20.17 -    (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
   20.18 +    (Parse_Spec.opt_thm_name ":"  -- Parse.thm --
   20.19        Scan.optional parse_splits [] >> simps_of_case_cmd)
   20.20  
   20.21  end
    21.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 13 17:00:02 2016 +0200
    21.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 13 18:01:05 2016 +0200
    21.3 @@ -536,7 +536,7 @@
    21.4        let
    21.5          val ref_of_str = (* FIXME proper wrapper for parser combinators *)
    21.6            suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
    21.7 -          #> Parse.xthm #> fst
    21.8 +          #> Parse.thm #> fst
    21.9          val thms = named_thms |> maps snd
   21.10          val facts = named_thms |> map (ref_of_str o fst o fst)
   21.11          val fact_override = {add = facts, del = [], only = true}
    22.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 13 17:00:02 2016 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 13 18:01:05 2016 +0200
    22.3 @@ -680,14 +680,14 @@
    22.4  val _ =
    22.5    Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
    22.6      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
    22.7 -    (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
    22.8 +    (Parse.name -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
    22.9        (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
   22.10          prove_strong_ind name avoids));
   22.11  
   22.12  val _ =
   22.13    Outer_Syntax.local_theory @{command_keyword equivariance}
   22.14      "prove equivariance for inductive predicate involving nominal datatypes"
   22.15 -    (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
   22.16 +    (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
   22.17        (fn (name, atoms) => prove_eqvt name atoms));
   22.18  
   22.19  end
    23.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 13 17:00:02 2016 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 13 18:01:05 2016 +0200
    23.3 @@ -488,7 +488,7 @@
    23.4  val _ =
    23.5    Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
    23.6      "prove strong induction theorem for inductive predicate involving nominal datatypes"
    23.7 -    (Parse.xname -- 
    23.8 +    (Parse.name -- 
    23.9       Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
   23.10       (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
   23.11        (@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
    24.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 17:00:02 2016 +0200
    24.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 18:01:05 2016 +0200
    24.3 @@ -51,7 +51,7 @@
    24.4  @{rail \<open>
    24.5    @'spark_types' ((name '=' type (mapping?))+)
    24.6    ;
    24.7 -  mapping: '('((name '=' nameref)+',')')'
    24.8 +  mapping: '('((name '=' name)+',')')'
    24.9  \<close>}
   24.10  Associates a \SPARK{} type with the given name with an Isabelle type. This command can
   24.11  only be used outside a verification environment. The given type must be either a record
    25.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 17:00:02 2016 +0200
    25.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 18:01:05 2016 +0200
    25.3 @@ -117,7 +117,7 @@
    25.4      "associate SPARK types with types"
    25.5      (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
    25.6         Scan.optional (Args.parens (Parse.list1
    25.7 -         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
    25.8 +         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >>
    25.9         (Toplevel.theory o fold add_spark_type_cmd));
   25.10  
   25.11  val _ =
    26.1 --- a/src/HOL/Statespace/state_space.ML	Wed Apr 13 17:00:02 2016 +0200
    26.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Apr 13 18:01:05 2016 +0200
    26.3 @@ -642,7 +642,7 @@
    26.4  
    26.5  val parent =
    26.6    Parse_Spec.locale_prefix --
    26.7 -  ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
    26.8 +  ((type_insts -- Parse.name) || (Parse.name >> pair [])) -- renames
    26.9      >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
   26.10  
   26.11  in
    27.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Wed Apr 13 17:00:02 2016 +0200
    27.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Wed Apr 13 18:01:05 2016 +0200
    27.3 @@ -426,7 +426,7 @@
    27.4    Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
    27.5      (K Plugin_Name.default_filter) >> Plugins_Option >> single;
    27.6  
    27.7 -val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.xthm);
    27.8 +val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
    27.9  
   27.10  in
   27.11  
    28.1 --- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 13 17:00:02 2016 +0200
    28.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Wed Apr 13 18:01:05 2016 +0200
    28.3 @@ -305,7 +305,7 @@
    28.4  val add_partial_function = gen_add_partial_function Specification.check_spec;
    28.5  val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
    28.6  
    28.7 -val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
    28.8 +val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
    28.9  
   28.10  val _ =
   28.11    Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
    29.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Apr 13 17:00:02 2016 +0200
    29.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Apr 13 18:01:05 2016 +0200
    29.3 @@ -812,7 +812,7 @@
    29.4        (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
    29.5            >> Scan.triple2) --
    29.6          (@{keyword "is"} |-- Parse.term) --
    29.7 -        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Scan.triple1)
    29.8 +        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.thms1) []) >> Scan.triple1)
    29.9       >> lift_def_cmd_with_err_handling);
   29.10  
   29.11  end
    30.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 13 17:00:02 2016 +0200
    30.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 13 18:01:05 2016 +0200
    30.3 @@ -809,8 +809,8 @@
    30.4  val _ = 
    30.5    Outer_Syntax.local_theory @{command_keyword setup_lifting}
    30.6      "setup lifting infrastructure" 
    30.7 -      (Parse.xthm -- Scan.option Parse.xthm 
    30.8 -      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
    30.9 +      (Parse.thm -- Scan.option Parse.thm 
   30.10 +      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm) >> 
   30.11          (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
   30.12            setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
   30.13  
   30.14 @@ -1024,7 +1024,7 @@
   30.15  val _ =
   30.16    Outer_Syntax.local_theory @{command_keyword lifting_forget} 
   30.17      "unsetup Lifting and Transfer for the given lifting bundle"
   30.18 -    (Parse.position Parse.xname >> (lifting_forget_cmd))
   30.19 +    (Parse.position Parse.name >> (lifting_forget_cmd))
   30.20  
   30.21  (* lifting_update *)
   30.22  
   30.23 @@ -1053,6 +1053,6 @@
   30.24  val _ =
   30.25    Outer_Syntax.local_theory @{command_keyword lifting_update}
   30.26      "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
   30.27 -    (Parse.position Parse.xname >> lifting_update_cmd)
   30.28 +    (Parse.position Parse.name >> lifting_update_cmd)
   30.29  
   30.30  end
    31.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 13 17:00:02 2016 +0200
    31.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 13 18:01:05 2016 +0200
    31.3 @@ -1030,7 +1030,7 @@
    31.4  (* values command for Prolog queries *)
    31.5  
    31.6  val opt_print_modes =
    31.7 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    31.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
    31.9  
   31.10  val _ =
   31.11    Outer_Syntax.command @{command_keyword values_prolog}
    32.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 13 17:00:02 2016 +0200
    32.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 13 18:01:05 2016 +0200
    32.3 @@ -222,12 +222,12 @@
    32.4      parse_mode_tuple_expr) xs
    32.5  
    32.6  val mode_and_opt_proposal = parse_mode_expr --
    32.7 -  Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
    32.8 +  Scan.optional (Args.$$$ "as" |-- Parse.name >> SOME) NONE
    32.9  
   32.10  
   32.11  val opt_modes =
   32.12    Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
   32.13 -    (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
   32.14 +    (((Parse.enum1 "and" (Parse.name --| @{keyword ":"} --
   32.15          (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
   32.16        || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
   32.17      --| @{keyword ")"}) (Multiple_Preds [])
   32.18 @@ -250,7 +250,7 @@
   32.19    end
   32.20  
   32.21  val opt_print_modes =
   32.22 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
   32.23 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
   32.24  
   32.25  val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
   32.26  
    33.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 13 17:00:02 2016 +0200
    33.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 13 18:01:05 2016 +0200
    33.3 @@ -348,7 +348,7 @@
    33.4          Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
    33.5            Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
    33.6          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
    33.7 -        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
    33.8 +        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm))
    33.9        >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
   33.10  
   33.11  end
    34.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 13 17:00:02 2016 +0200
    34.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 13 18:01:05 2016 +0200
    34.3 @@ -349,10 +349,10 @@
    34.4  
    34.5  val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
    34.6  val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
    34.7 -val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
    34.8 +val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
    34.9  val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   34.10  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   34.11 -val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.xthm)
   34.12 +val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
   34.13  val parse_fact_override_chunk =
   34.14    (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   34.15    || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
    35.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 13 17:00:02 2016 +0200
    35.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 13 18:01:05 2016 +0200
    35.3 @@ -129,7 +129,7 @@
    35.4      |> Symbol.source
    35.5      |> Token.source keywords Position.start
    35.6      |> Token.source_proper
    35.7 -    |> Source.source Token.stopper (Parse.xthms1 >> get)
    35.8 +    |> Source.source Token.stopper (Parse.thms1 >> get)
    35.9      |> Source.exhaust
   35.10    end
   35.11  
    36.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 13 17:00:02 2016 +0200
    36.2 +++ b/src/HOL/Tools/inductive.ML	Wed Apr 13 18:01:05 2016 +0200
    36.3 @@ -1182,7 +1182,7 @@
    36.4  fun gen_ind_decl mk_def coind =
    36.5    Parse.fixes -- Parse.for_fixes --
    36.6    Scan.optional Parse_Spec.where_alt_specs [] --
    36.7 -  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []
    36.8 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
    36.9    >> (fn (((preds, params), specs), monos) =>
   36.10        (snd o gen_add_inductive mk_def true coind preds params specs monos));
   36.11  
    37.1 --- a/src/HOL/Tools/record.ML	Wed Apr 13 17:00:02 2016 +0200
    37.2 +++ b/src/HOL/Tools/record.ML	Wed Apr 13 18:01:05 2016 +0200
    37.3 @@ -2411,7 +2411,7 @@
    37.4          Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
    37.5  
    37.6  val opt_modes =
    37.7 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    37.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
    37.9  
   37.10  val _ =
   37.11    Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
    38.1 --- a/src/HOL/Tools/try0.ML	Wed Apr 13 17:00:02 2016 +0200
    38.2 +++ b/src/HOL/Tools/try0.ML	Wed Apr 13 18:01:05 2016 +0200
    38.3 @@ -166,7 +166,7 @@
    38.4    implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
    38.5  
    38.6  val parse_fact_refs =
    38.7 -  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
    38.8 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm));
    38.9  
   38.10  val parse_attr =
   38.11    Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
    39.1 --- a/src/HOL/Tools/value.ML	Wed Apr 13 17:00:02 2016 +0200
    39.2 +++ b/src/HOL/Tools/value.ML	Wed Apr 13 18:01:05 2016 +0200
    39.3 @@ -64,10 +64,10 @@
    39.4    in Pretty.writeln p end;
    39.5  
    39.6  val opt_modes =
    39.7 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    39.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
    39.9  
   39.10  val opt_evaluator =
   39.11 -  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
   39.12 +  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
   39.13    
   39.14  val _ =
   39.15    Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    40.1 --- a/src/Pure/General/completion.scala	Wed Apr 13 17:00:02 2016 +0200
    40.2 +++ b/src/Pure/General/completion.scala	Wed Apr 13 18:01:05 2016 +0200
    40.3 @@ -209,7 +209,7 @@
    40.4            val description = List(xname1, "(" + descr_name + ")")
    40.5            val replacement =
    40.6              Token.explode(Keyword.Keywords.empty, xname1) match {
    40.7 -              case List(tok) if tok.is_xname => xname1
    40.8 +              case List(tok) if tok.is_name => xname1
    40.9                case _ => quote(xname1)
   40.10              }
   40.11            Item(range, original, full_name, description, replacement, 0, true)
    41.1 --- a/src/Pure/Isar/method.ML	Wed Apr 13 17:00:02 2016 +0200
    41.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 13 18:01:05 2016 +0200
    41.3 @@ -599,7 +599,7 @@
    41.4  local
    41.5  
    41.6  fun sect (modifier : modifier parser) = Scan.depend (fn context =>
    41.7 -  Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.xthm)
    41.8 +  Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.thm)
    41.9      >> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) =>
   41.10        let
   41.11          val decl =
   41.12 @@ -689,7 +689,7 @@
   41.13  
   41.14  fun parser pri =
   41.15    let
   41.16 -    val meth_name = Parse.token Parse.xname;
   41.17 +    val meth_name = Parse.token Parse.name;
   41.18  
   41.19      fun meth5 x =
   41.20       (meth_name >> (Source o single) ||
    42.1 --- a/src/Pure/Isar/parse.ML	Wed Apr 13 17:00:02 2016 +0200
    42.2 +++ b/src/Pure/Isar/parse.ML	Wed Apr 13 18:01:05 2016 +0200
    42.3 @@ -64,12 +64,10 @@
    42.4    val properties: Properties.T parser
    42.5    val name: bstring parser
    42.6    val binding: binding parser
    42.7 -  val xname: xstring parser
    42.8    val text: string parser
    42.9    val path: string parser
   42.10 -  val theory_name: bstring parser
   42.11 -  val theory_xname: xstring parser
   42.12 -  val liberal_name: xstring parser
   42.13 +  val theory_name: string parser
   42.14 +  val liberal_name: string parser
   42.15    val parname: string parser
   42.16    val parbinding: binding parser
   42.17    val class: string parser
   42.18 @@ -104,15 +102,15 @@
   42.19    val termp: (string * string list) parser
   42.20    val private: Position.T parser
   42.21    val qualified: Position.T parser
   42.22 -  val target: (xstring * Position.T) parser
   42.23 -  val opt_target: (xstring * Position.T) option parser
   42.24 +  val target: (string * Position.T) parser
   42.25 +  val opt_target: (string * Position.T) option parser
   42.26    val args: Token.T list parser
   42.27    val args1: (string -> bool) -> Token.T list parser
   42.28    val attribs: Token.src list parser
   42.29    val opt_attribs: Token.src list parser
   42.30    val thm_sel: Facts.interval list parser
   42.31 -  val xthm: (Facts.ref * Token.src list) parser
   42.32 -  val xthms1: (Facts.ref * Token.src list) list parser
   42.33 +  val thm: (Facts.ref * Token.src list) parser
   42.34 +  val thms1: (Facts.ref * Token.src list) list parser
   42.35  end;
   42.36  
   42.37  structure Parse: PARSE =
   42.38 @@ -261,22 +259,20 @@
   42.39  
   42.40  (* names and text *)
   42.41  
   42.42 -val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
   42.43 +val name =
   42.44 +  group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
   42.45  
   42.46  val binding = position name >> Binding.make;
   42.47  
   42.48 -val xname = group (fn () => "name reference")
   42.49 -  (short_ident || long_ident || sym_ident || string || number);
   42.50 +val text =
   42.51 +  group (fn () => "text")
   42.52 +    (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
   42.53  
   42.54 -val text = group (fn () => "text")
   42.55 -  (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
   42.56 -
   42.57 -val path = group (fn () => "file name/path specification") xname;
   42.58 +val path = group (fn () => "file name/path specification") name;
   42.59  
   42.60  val theory_name = group (fn () => "theory name") name;
   42.61 -val theory_xname = group (fn () => "theory name reference") xname;
   42.62  
   42.63 -val liberal_name = keyword_with Token.ident_or_symbolic || xname;
   42.64 +val liberal_name = keyword_with Token.ident_or_symbolic || name;
   42.65  
   42.66  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   42.67  val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
   42.68 @@ -284,11 +280,11 @@
   42.69  
   42.70  (* type classes *)
   42.71  
   42.72 -val class = group (fn () => "type class") (inner_syntax xname);
   42.73 +val class = group (fn () => "type class") (inner_syntax name);
   42.74  
   42.75 -val sort = group (fn () => "sort") (inner_syntax xname);
   42.76 +val sort = group (fn () => "sort") (inner_syntax name);
   42.77  
   42.78 -val type_const = inner_syntax (group (fn () => "type constructor") xname);
   42.79 +val type_const = inner_syntax (group (fn () => "type constructor") name);
   42.80  
   42.81  val arity = type_const -- ($$$ "::" |-- !!!
   42.82    (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
   42.83 @@ -398,7 +394,7 @@
   42.84  val term = inner_syntax term_group;
   42.85  val prop = inner_syntax prop_group;
   42.86  
   42.87 -val const = inner_syntax (group (fn () => "constant") xname);
   42.88 +val const = inner_syntax (group (fn () => "constant") name);
   42.89  
   42.90  val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
   42.91  
   42.92 @@ -417,7 +413,7 @@
   42.93  val private = position ($$$ "private") >> #2;
   42.94  val qualified = position ($$$ "qualified") >> #2;
   42.95  
   42.96 -val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
   42.97 +val target = ($$$ "(" -- $$$ "in") |-- !!! (position name --| $$$ ")");
   42.98  val opt_target = Scan.option target;
   42.99  
  42.100  
  42.101 @@ -468,11 +464,11 @@
  42.102    nat --| minus >> Facts.From ||
  42.103    nat >> Facts.Single) --| $$$ ")";
  42.104  
  42.105 -val xthm =
  42.106 +val thm =
  42.107    $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
  42.108    (literal_fact >> Facts.Fact ||
  42.109 -    position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
  42.110 +    position name -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
  42.111  
  42.112 -val xthms1 = Scan.repeat1 xthm;
  42.113 +val thms1 = Scan.repeat1 thm;
  42.114  
  42.115  end;
    43.1 --- a/src/Pure/Isar/parse.scala	Wed Apr 13 17:00:02 2016 +0200
    43.2 +++ b/src/Pure/Isar/parse.scala	Wed Apr 13 18:01:05 2016 +0200
    43.3 @@ -67,19 +67,16 @@
    43.4  
    43.5      def string: Parser[String] = atom("string", _.is_string)
    43.6      def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
    43.7 -    def name: Parser[String] = atom("name declaration", _.is_name)
    43.8 -    def xname: Parser[String] = atom("name reference", _.is_xname)
    43.9 +    def name: Parser[String] = atom("name", _.is_name)
   43.10      def text: Parser[String] = atom("text", _.is_text)
   43.11      def ML_source: Parser[String] = atom("ML source", _.is_text)
   43.12      def document_source: Parser[String] = atom("document source", _.is_text)
   43.13  
   43.14      def path: Parser[String] =
   43.15 -      atom("file name/path specification", tok => tok.is_xname && Path.is_wellformed(tok.content))
   43.16 +      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
   43.17  
   43.18      def theory_name: Parser[String] =
   43.19        atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
   43.20 -    def theory_xname: Parser[String] =
   43.21 -      atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content))
   43.22  
   43.23      private def tag_name: Parser[String] =
   43.24        atom("tag name", tok =>
    44.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Apr 13 17:00:02 2016 +0200
    44.2 +++ b/src/Pure/Isar/parse_spec.ML	Wed Apr 13 18:01:05 2016 +0200
    44.3 @@ -55,7 +55,7 @@
    44.4  
    44.5  val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    44.6  
    44.7 -val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1);
    44.8 +val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1);
    44.9  
   44.10  
   44.11  (* basic constant specifications *)
   44.12 @@ -72,7 +72,7 @@
   44.13  
   44.14  (* locale and context elements *)
   44.15  
   44.16 -val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
   44.17 +val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name));
   44.18  
   44.19  val locale_fixes =
   44.20    Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
   44.21 @@ -95,7 +95,7 @@
   44.22      >> Element.Assumes ||
   44.23    Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   44.24      >> Element.Defines ||
   44.25 -  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1))
   44.26 +  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.thms1))
   44.27      >> (curry Element.Notes "");
   44.28  
   44.29  fun plus1_unless test scan =
   44.30 @@ -120,7 +120,7 @@
   44.31  
   44.32  val locale_expression =
   44.33    let
   44.34 -    val expr2 = Parse.position Parse.xname;
   44.35 +    val expr2 = Parse.position Parse.name;
   44.36      val expr1 =
   44.37        locale_prefix -- expr2 --
   44.38        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    45.1 --- a/src/Pure/Isar/token.ML	Wed Apr 13 17:00:02 2016 +0200
    45.2 +++ b/src/Pure/Isar/token.ML	Wed Apr 13 18:01:05 2016 +0200
    45.3 @@ -38,7 +38,6 @@
    45.4    val kind_of: T -> kind
    45.5    val is_kind: kind -> T -> bool
    45.6    val is_command: T -> bool
    45.7 -  val is_name: T -> bool
    45.8    val keyword_with: (string -> bool) -> T -> bool
    45.9    val is_command_modifier: T -> bool
   45.10    val ident_with: (string -> bool) -> T -> bool
   45.11 @@ -210,8 +209,6 @@
   45.12  
   45.13  val is_command = is_kind Command;
   45.14  
   45.15 -val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
   45.16 -
   45.17  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   45.18    | keyword_with _ _ = false;
   45.19  
    46.1 --- a/src/Pure/Isar/token.scala	Wed Apr 13 17:00:02 2016 +0200
    46.2 +++ b/src/Pure/Isar/token.scala	Wed Apr 13 18:01:05 2016 +0200
    46.3 @@ -236,11 +236,11 @@
    46.4    def is_float: Boolean = kind == Token.Kind.FLOAT
    46.5    def is_name: Boolean =
    46.6      kind == Token.Kind.IDENT ||
    46.7 +    kind == Token.Kind.LONG_IDENT ||
    46.8      kind == Token.Kind.SYM_IDENT ||
    46.9      kind == Token.Kind.STRING ||
   46.10      kind == Token.Kind.NAT
   46.11 -  def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
   46.12 -  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   46.13 +  def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   46.14    def is_space: Boolean = kind == Token.Kind.SPACE
   46.15    def is_comment: Boolean = kind == Token.Kind.COMMENT
   46.16    def is_improper: Boolean = is_space || is_comment
    47.1 --- a/src/Pure/ML/ml_context.ML	Wed Apr 13 17:00:02 2016 +0200
    47.2 +++ b/src/Pure/ML/ml_context.ML	Wed Apr 13 18:01:05 2016 +0200
    47.3 @@ -96,7 +96,7 @@
    47.4  local
    47.5  
    47.6  val antiq =
    47.7 -  Parse.!!! ((Parse.token Parse.xname ::: Parse.args) --| Scan.ahead Parse.eof);
    47.8 +  Parse.!!! ((Parse.token Parse.name ::: Parse.args) --| Scan.ahead Parse.eof);
    47.9  
   47.10  fun make_env name visible =
   47.11    (ML_Lex.tokenize
    48.1 --- a/src/Pure/PIDE/command.scala	Wed Apr 13 17:00:02 2016 +0200
    48.2 +++ b/src/Pure/PIDE/command.scala	Wed Apr 13 18:01:05 2016 +0200
    48.3 @@ -322,7 +322,7 @@
    48.4    private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
    48.5      if (tokens.exists({ case (t, _) => t.is_command })) {
    48.6        tokens.dropWhile({ case (t, _) => !t.is_command }).
    48.7 -        collectFirst({ case (t, i) if t.is_xname => (t.content, i) })
    48.8 +        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    48.9      }
   48.10      else None
   48.11  
    49.1 --- a/src/Pure/Pure.thy	Wed Apr 13 17:00:02 2016 +0200
    49.2 +++ b/src/Pure/Pure.thy	Wed Apr 13 18:01:05 2016 +0200
    49.3 @@ -280,7 +280,7 @@
    49.4  
    49.5  val trans_pat =
    49.6    Scan.optional
    49.7 -    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
    49.8 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
    49.9      -- Parse.inner_syntax Parse.string;
   49.10  
   49.11  fun trans_arrow toks =
   49.12 @@ -403,7 +403,7 @@
   49.13  
   49.14  val _ =
   49.15    Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   49.16 -    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   49.17 +    (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
   49.18        >> (fn (facts, fixes) =>
   49.19            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   49.20  
   49.21 @@ -442,7 +442,7 @@
   49.22  
   49.23  val _ =
   49.24    hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   49.25 -    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   49.26 +    (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
   49.27  
   49.28  in end\<close>
   49.29  
   49.30 @@ -454,18 +454,18 @@
   49.31  
   49.32  val _ =
   49.33    Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
   49.34 -    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
   49.35 +    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
   49.36        >> (uncurry Bundle.bundle_cmd));
   49.37  
   49.38  val _ =
   49.39    Outer_Syntax.command @{command_keyword include}
   49.40      "include declarations from bundle in proof body"
   49.41 -    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
   49.42 +    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
   49.43  
   49.44  val _ =
   49.45    Outer_Syntax.command @{command_keyword including}
   49.46      "include declarations from bundle in goal refinement"
   49.47 -    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
   49.48 +    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
   49.49  
   49.50  val _ =
   49.51    Outer_Syntax.command @{command_keyword print_bundles}
   49.52 @@ -484,7 +484,7 @@
   49.53  
   49.54  val _ =
   49.55    Outer_Syntax.command @{command_keyword context} "begin local theory context"
   49.56 -    ((Parse.position Parse.xname >> (fn name =>
   49.57 +    ((Parse.position Parse.name >> (fn name =>
   49.58          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
   49.59        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
   49.60          >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
   49.61 @@ -550,7 +550,7 @@
   49.62  val _ =
   49.63    Outer_Syntax.command @{command_keyword sublocale}
   49.64      "prove sublocale relation between a locale and a locale expression"
   49.65 -    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
   49.66 +    ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
   49.67        interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
   49.68          Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
   49.69      || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   49.70 @@ -684,7 +684,7 @@
   49.71  ML \<open>
   49.72  local
   49.73  
   49.74 -val facts = Parse.and_list1 Parse.xthms1;
   49.75 +val facts = Parse.and_list1 Parse.thms1;
   49.76  
   49.77  val _ =
   49.78    Outer_Syntax.command @{command_keyword then} "forward chaining"
   49.79 @@ -773,9 +773,9 @@
   49.80    Outer_Syntax.command @{command_keyword case} "invoke local context"
   49.81      (Parse_Spec.opt_thm_name ":" --
   49.82        (@{keyword "("} |--
   49.83 -        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
   49.84 +        Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
   49.85            --| @{keyword ")"}) ||
   49.86 -        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   49.87 +        Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   49.88  
   49.89  in end\<close>
   49.90  
   49.91 @@ -906,7 +906,7 @@
   49.92  local
   49.93  
   49.94  val calculation_args =
   49.95 -  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
   49.96 +  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
   49.97  
   49.98  val _ =
   49.99    Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
  49.100 @@ -956,7 +956,7 @@
  49.101  local
  49.102  
  49.103  val opt_modes =
  49.104 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
  49.105 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
  49.106  
  49.107  val _ =
  49.108    Outer_Syntax.command @{command_keyword help}
  49.109 @@ -1025,13 +1025,13 @@
  49.110  val _ =
  49.111    Outer_Syntax.command @{command_keyword print_locale}
  49.112      "print locale of this theory"
  49.113 -    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
  49.114 +    (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
  49.115        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  49.116  
  49.117  val _ =
  49.118    Outer_Syntax.command @{command_keyword print_interps}
  49.119      "print interpretations of locale for this theory or proof context"
  49.120 -    (Parse.position Parse.xname >> (fn name =>
  49.121 +    (Parse.position Parse.name >> (fn name =>
  49.122        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  49.123  
  49.124  val _ =
  49.125 @@ -1100,19 +1100,19 @@
  49.126  val _ =
  49.127    Outer_Syntax.command @{command_keyword print_statement}
  49.128      "print theorems as long statements"
  49.129 -    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
  49.130 +    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
  49.131  
  49.132  val _ =
  49.133    Outer_Syntax.command @{command_keyword thm} "print theorems"
  49.134 -    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
  49.135 +    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
  49.136  
  49.137  val _ =
  49.138    Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
  49.139 -    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
  49.140 +    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
  49.141  
  49.142  val _ =
  49.143    Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
  49.144 -    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
  49.145 +    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
  49.146  
  49.147  val _ =
  49.148    Outer_Syntax.command @{command_keyword prop} "read and print proposition"
  49.149 @@ -1156,8 +1156,8 @@
  49.150  local
  49.151  
  49.152  val theory_bounds =
  49.153 -  Parse.position Parse.theory_xname >> single ||
  49.154 -  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
  49.155 +  Parse.position Parse.theory_name >> single ||
  49.156 +  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
  49.157  
  49.158  val _ =
  49.159    Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  49.160 @@ -1177,14 +1177,14 @@
  49.161  
  49.162  val _ =
  49.163    Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
  49.164 -    (Parse.xthms1 >> (fn args =>
  49.165 +    (Parse.thms1 >> (fn args =>
  49.166        Toplevel.keep (fn st =>
  49.167          Thm_Deps.thm_deps (Toplevel.theory_of st)
  49.168            (Attrib.eval_thms (Toplevel.context_of st) args))));
  49.169  
  49.170  
  49.171  val thy_names =
  49.172 -  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
  49.173 +  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
  49.174  
  49.175  val _ =
  49.176    Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
  49.177 @@ -1260,7 +1260,7 @@
  49.178  val _ =
  49.179    Outer_Syntax.command @{command_keyword realizers}
  49.180      "specify realizers for primitive axioms / theorems, together with correctness proof"
  49.181 -    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  49.182 +    (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  49.183       (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  49.184         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  49.185  
  49.186 @@ -1276,7 +1276,7 @@
  49.187  
  49.188  val _ =
  49.189    Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  49.190 -    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  49.191 +    (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  49.192        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  49.193  
  49.194  in end\<close>
    50.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 13 17:00:02 2016 +0200
    50.2 +++ b/src/Pure/Thy/sessions.scala	Wed Apr 13 18:01:05 2016 +0200
    50.3 @@ -201,7 +201,7 @@
    50.4  
    50.5        val theories =
    50.6          ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
    50.7 -          ((options | success(Nil)) ~ rep(theory_xname)) ^^
    50.8 +          ((options | success(Nil)) ~ rep(theory_name)) ^^
    50.9            { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
   50.10  
   50.11        val document_files =
    51.1 --- a/src/Pure/Thy/term_style.ML	Wed Apr 13 17:00:02 2016 +0200
    51.2 +++ b/src/Pure/Thy/term_style.ML	Wed Apr 13 18:01:05 2016 +0200
    51.3 @@ -32,7 +32,7 @@
    51.4  (* style parsing *)
    51.5  
    51.6  fun parse_single ctxt =
    51.7 -  Parse.token Parse.xname ::: Parse.args >> (fn src0 =>
    51.8 +  Parse.token Parse.name ::: Parse.args >> (fn src0 =>
    51.9      let
   51.10        val (src, parse) = Token.check_src ctxt get_data src0;
   51.11        val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
    52.1 --- a/src/Pure/Thy/thy_header.ML	Wed Apr 13 17:00:02 2016 +0200
    52.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Apr 13 18:01:05 2016 +0200
    52.3 @@ -117,7 +117,7 @@
    52.4  
    52.5  fun imports name =
    52.6    if name = Context.PureN then Scan.succeed []
    52.7 -  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
    52.8 +  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
    52.9  
   52.10  val opt_files =
   52.11    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
    53.1 --- a/src/Pure/Thy/thy_header.scala	Wed Apr 13 17:00:02 2016 +0200
    53.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Apr 13 18:01:05 2016 +0200
    53.3 @@ -109,7 +109,7 @@
    53.4  
    53.5      val args =
    53.6        position(theory_name) ~
    53.7 -      (opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^
    53.8 +      (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
    53.9          { case None => Nil case Some(_ ~ xs) => xs }) ~
   53.10        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   53.11          { case None => Nil case Some(_ ~ xs) => xs }) ~
    54.1 --- a/src/Pure/Thy/thy_output.ML	Wed Apr 13 17:00:02 2016 +0200
    54.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Apr 13 18:01:05 2016 +0200
    54.3 @@ -143,7 +143,7 @@
    54.4  local
    54.5  
    54.6  val property =
    54.7 -  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
    54.8 +  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
    54.9  
   54.10  val properties =
   54.11    Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
   54.12 @@ -404,7 +404,7 @@
   54.13  
   54.14  val locale =
   54.15    Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
   54.16 -    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
   54.17 +    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
   54.18  
   54.19  in
   54.20  
    55.1 --- a/src/Pure/Tools/find_consts.ML	Wed Apr 13 17:00:02 2016 +0200
    55.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Apr 13 18:01:05 2016 +0200
    55.3 @@ -136,7 +136,7 @@
    55.4  local
    55.5  
    55.6  val criterion =
    55.7 -  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    55.8 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
    55.9    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
   55.10    Parse.typ >> Loose;
   55.11  
    56.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Apr 13 17:00:02 2016 +0200
    56.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 13 18:01:05 2016 +0200
    56.3 @@ -509,7 +509,7 @@
    56.4  local
    56.5  
    56.6  val criterion =
    56.7 -  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    56.8 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
    56.9    Parse.reserved "intro" >> K Intro ||
   56.10    Parse.reserved "elim" >> K Elim ||
   56.11    Parse.reserved "dest" >> K Dest ||
    57.1 --- a/src/Tools/Code/code_target.ML	Wed Apr 13 17:00:02 2016 +0200
    57.2 +++ b/src/Tools/Code/code_target.ML	Wed Apr 13 18:01:05 2016 +0200
    57.3 @@ -104,7 +104,7 @@
    57.4  fun read_inst ctxt (raw_tyco, raw_class) =
    57.5    (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
    57.6  
    57.7 -val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
    57.8 +val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class;
    57.9  
   57.10  fun cert_syms ctxt =
   57.11    Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
    58.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Apr 13 17:00:02 2016 +0200
    58.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Apr 13 18:01:05 2016 +0200
    58.3 @@ -433,9 +433,9 @@
    58.4      ("define " ^ coind_prefix ^ "datatype")
    58.5      ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
    58.6        Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
    58.7 -      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
    58.8 -      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
    58.9 -      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
   58.10 +      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
   58.11 +      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
   58.12 +      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
   58.13        >> (Toplevel.theory o mk_datatype));
   58.14  
   58.15  end;
    59.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 17:00:02 2016 +0200
    59.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:01:05 2016 +0200
    59.3 @@ -192,10 +192,10 @@
    59.4  
    59.5  val _ =
    59.6    Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
    59.7 -    ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
    59.8 -     (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
    59.9 -     (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
   59.10 -     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.xthms1) []
   59.11 +    ((@{keyword "elimination"} |-- Parse.!!! Parse.thm) --
   59.12 +     (@{keyword "induction"} |-- Parse.!!! Parse.thm) --
   59.13 +     (@{keyword "case_eqns"} |-- Parse.!!! Parse.thms1) --
   59.14 +     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.thms1) []
   59.15       >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
   59.16  
   59.17  end;
    60.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Apr 13 17:00:02 2016 +0200
    60.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Apr 13 18:01:05 2016 +0200
    60.3 @@ -587,10 +587,10 @@
    60.4        ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
    60.5    (@{keyword "intros"} |--
    60.6      Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
    60.7 -  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
    60.8 -  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.xthms1) [] --
    60.9 -  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
   60.10 -  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
   60.11 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
   60.12 +  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.thms1) [] --
   60.13 +  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
   60.14 +  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
   60.15    >> (Toplevel.theory o mk_ind);
   60.16  
   60.17  val _ =