# HG changeset patch
# User wenzelm
# Date 1460563265 -7200
# Node ID 9f394a16c557410fb2a530b06e8a9a6d4e47d08b
# Parent  4e4738698db4755cdaf6d9a3e5d1ef47658db255
eliminated "xname" and variants;

diff -r 4e4738698db4 -r 9f394a16c557 NEWS
--- a/NEWS	Wed Apr 13 17:00:02 2016 +0200
+++ b/NEWS	Wed Apr 13 18:01:05 2016 +0200
@@ -16,6 +16,10 @@
 INCOMPATIBILITY, need to provide explicit type constraints for Pure
 types where this is really intended.
 
+* Simplified outer syntax: uniform category "name" includes long
+identifiers. Former "xname" / "nameref" / "name reference" has been
+discontinued.
+
 * Mixfix annotations support general block properties, with syntax
 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -3020,7 +3020,7 @@
 @{rail \<open>
   @@{command lift_bnf} target? lb_options? \<newline>
     @{syntax tyargs} name wit_terms?  \<newline>
-    ('via' thmref)? @{syntax map_rel}?
+    ('via' thm)? @{syntax map_rel}?
   ;
   @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
   ;
@@ -3055,7 +3055,7 @@
 
 @{rail \<open>
   @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
-    @{syntax tyargs} name ('via' thmref)? @{syntax map_rel}?
+    @{syntax tyargs} name ('via' thm)? @{syntax map_rel}?
 \<close>}
 \medskip
 
@@ -3203,7 +3203,7 @@
 
 @{rail \<open>
   @@{command simps_of_case} target? (name ':')? \<newline>
-    (thmref + ) (@'splits' ':' (thmref + ))?
+    (thm + ) (@'splits' ':' (thm + ))?
 \<close>}
 
 \medskip
@@ -3242,7 +3242,7 @@
 
 @{rail \<open>
   @@{command case_of_simps} target? (name ':')? \<newline>
-    (thmref + )
+    (thm + )
 \<close>}
 
 \medskip
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Eisbach/Manual.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -288,7 +288,7 @@
     ;
     kind:
       (@'conclusion' | @'premises' ('(' 'local' ')')? |
-       '(' term ')' | @{syntax thmrefs})
+       '(' term ')' | @{syntax thms})
     ;
     pattern: fact_name? term args? \<newline> (@'for' fixes)?
     ;
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/Isar.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -363,7 +363,7 @@
 
   The @{ML Attrib.thms} parser produces a list of theorems from the usual Isar
   syntax involving attribute expressions etc.\ (syntax category @{syntax
-  thmrefs}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
+  thms}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
   added to @{ML HOL_basic_ss} which already contains the basic Simplifier
   setup for HOL.
 
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -171,13 +171,13 @@
   \end{matharray}
 
   @{rail \<open>
-  @@{ML_antiquotation class} nameref
+  @@{ML_antiquotation class} name
   ;
   @@{ML_antiquotation sort} sort
   ;
   (@@{ML_antiquotation type_name} |
    @@{ML_antiquotation type_abbrev} |
-   @@{ML_antiquotation nonterminal}) nameref
+   @@{ML_antiquotation nonterminal}) name
   ;
   @@{ML_antiquotation typ} type
   \<close>}
@@ -392,7 +392,7 @@
 
   @{rail \<open>
   (@@{ML_antiquotation const_name} |
-   @@{ML_antiquotation const_abbrev}) nameref
+   @@{ML_antiquotation const_abbrev}) name
   ;
   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   ;
@@ -701,9 +701,9 @@
   ;
   @@{ML_antiquotation cprop} prop
   ;
-  @@{ML_antiquotation thm} thmref
+  @@{ML_antiquotation thm} thm
   ;
-  @@{ML_antiquotation thms} thmrefs
+  @@{ML_antiquotation thms} thms
   ;
   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
     @'by' method method?
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -653,10 +653,10 @@
   special syntactic entities of the following form:
 
   @{rail \<open>
-  @{syntax_def antiquote}: '@{' nameref args '}'
+  @{syntax_def antiquote}: '@{' name args '}'
   \<close>}
 
-  Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
+  Here @{syntax name} and @{syntax args} are outer syntax categories, as
   defined in @{cite "isabelle-isar-ref"}.
 
   \<^medskip>
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -142,9 +142,9 @@
   \end{matharray}
 
   @{rail \<open>
-  @@{ML_antiquotation theory} nameref?
+  @@{ML_antiquotation theory} name?
   ;
-  @@{ML_antiquotation theory_context} nameref
+  @@{ML_antiquotation theory_context} name
   \<close>}
 
   \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -167,7 +167,7 @@
       (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
         options @{syntax text} |
       @@{antiquotation theory} options @{syntax name} |
-      @@{antiquotation thm} options styles @{syntax thmrefs} |
+      @@{antiquotation thm} options styles @{syntax thms} |
       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
       @@{antiquotation prop} options styles @{syntax prop} |
       @@{antiquotation term} options styles @{syntax term} |
@@ -185,8 +185,8 @@
     @{syntax antiquotation}:
       @@{antiquotation goals} options |
       @@{antiquotation subgoals} options |
-      @@{antiquotation prf} options @{syntax thmrefs} |
-      @@{antiquotation full_prf} options @{syntax thmrefs} |
+      @@{antiquotation prf} options @{syntax thms} |
+      @@{antiquotation full_prf} options @{syntax thms} |
       @@{antiquotation ML} options @{syntax text} |
       @@{antiquotation ML_op} options @{syntax text} |
       @@{antiquotation ML_type} options @{syntax text} |
@@ -195,8 +195,8 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation "file"} options @{syntax xname} |
-      @@{antiquotation file_unchecked} options @{syntax xname} |
+      @@{antiquotation "file"} options @{syntax name} |
+      @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
@@ -613,7 +613,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command display_drafts} (@{syntax xname} +)
+    @@{command display_drafts} (@{syntax name} +)
   \<close>}
 
   \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -71,12 +71,12 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
+    (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thms}
     ;
     (@@{method erule} | @@{method drule} | @@{method frule})
-      ('(' @{syntax nat} ')')? @{syntax thmrefs}
+      ('(' @{syntax nat} ')')? @{syntax thms}
     ;
-    (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
+    (@@{method intro} | @@{method elim}) @{syntax thms}?
     ;
     @@{method sleep} @{syntax real}
   \<close>}
@@ -140,9 +140,9 @@
     ;
     @@{attribute untagged} @{syntax name}
     ;
-    @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
+    @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thm}
     ;
-    (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
+    (@@{attribute unfolded} | @@{attribute folded}) @{syntax thms}
     ;
     @@{attribute rotated} @{syntax int}?
   \<close>}
@@ -192,9 +192,9 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
+    @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thm}
     ;
-    @@{method split} @{syntax thmrefs}
+    @@{method split} @{syntax thms}
   \<close>}
 
   These methods provide low-level facilities for equational reasoning
@@ -284,7 +284,7 @@
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
-      'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
+      'cong' (() | 'add' | 'del')) ':' @{syntax thms}
   \<close>}
 
   \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
@@ -1063,7 +1063,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{attribute simplified} opt? @{syntax thmrefs}?
+    @@{attribute simplified} opt? @{syntax thms}?
     ;
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
@@ -1383,7 +1383,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method rule} @{syntax thmrefs}?
+    @@{method rule} @{syntax thms}?
   \<close>}
 
   \<^descr> @{method rule} as offered by the Classical Reasoner is a
@@ -1434,12 +1434,12 @@
     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
     ;
     @{syntax_def clamod}:
-      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
+      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thms}
     ;
     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
       ('cong' | 'split') (() | 'add' | 'del') |
       'iff' (((() | 'add') '?'?) | 'del') |
-      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
+      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thms}
   \<close>}
 
   \<^descr> @{method blast} is a separate classical tableau prover that
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -109,7 +109,7 @@
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
       @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
-      (@'where' clauses)? (@'monos' @{syntax thmrefs})?
+      (@'where' clauses)? (@'monos' @{syntax thms})?
     ;
     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
@@ -568,7 +568,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+    @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
       @'where' @{syntax thmdecl}? @{syntax prop}
   \<close>}
 
@@ -638,7 +638,7 @@
     hints: '(' @'hints' ( recdefmod * ) ')'
     ;
     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
-      (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
+      (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
   \<close>}
 
   \<^descr> @{command (HOL) "recdef"} defines general well-founded
@@ -689,7 +689,7 @@
 
   @{rail \<open>
     (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
-      (@{syntax nameref} (@{syntax term} + ) + @'and')
+      (@{syntax name} (@{syntax term} + ) + @'and')
   \<close>}
 
   \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close>
@@ -1265,7 +1265,7 @@
     ;
     quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
     ;
-    quot_parametric: @'parametric' @{syntax thmref}
+    quot_parametric: @'parametric' @{syntax thm}
   \<close>}
 
   \<^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)
@@ -1321,19 +1321,19 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
-      (@'parametric' @{syntax thmref})?
+    @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? \<newline>
+      (@'parametric' @{syntax thm})?
     ;
     @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
       @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
-      (@'parametric' (@{syntax thmref}+))?
+      (@'parametric' (@{syntax thm}+))?
     ;
-    @@{command (HOL) lifting_forget} @{syntax nameref}
+    @@{command (HOL) lifting_forget} @{syntax name}
     ;
-    @@{command (HOL) lifting_update} @{syntax nameref}
+    @@{command (HOL) lifting_update} @{syntax name}
     ;
     @@{attribute (HOL) lifting_restore}
-      @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
+      @{syntax thm} (@{syntax thm} @{syntax thm})?
   \<close>}
 
   \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
@@ -1661,9 +1661,9 @@
     ;
     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
     ;
-    @@{method (HOL) lifting} @{syntax thmrefs}?
+    @@{method (HOL) lifting} @{syntax thms}?
     ;
-    @@{method (HOL) lifting_setup} @{syntax thmrefs}?
+    @@{method (HOL) lifting_setup} @{syntax thms}?
   \<close>}
 
   \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the
@@ -1750,7 +1750,7 @@
     @@{command (HOL) try}
     ;
 
-    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
+    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
       @{syntax nat}?
     ;
 
@@ -1761,7 +1761,7 @@
     ;
     args: ( @{syntax name} '=' value + ',' )
     ;
-    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
+    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
   \<close>} % FIXME check args "value"
 
   \<^descr> @{command (HOL) "solve_direct"} checks whether the current
@@ -1822,7 +1822,7 @@
       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
     ;
 
-    @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>
+    @@{command (HOL) quickcheck_generator} @{syntax name} \<newline>
       'operations:' ( @{syntax term} +)
     ;
 
@@ -2140,11 +2140,11 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method (HOL) meson} @{syntax thmrefs}?
+    @@{method (HOL) meson} @{syntax thms}?
     ;
     @@{method (HOL) metis}
       ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
-      @{syntax thmrefs}?
+      @{syntax thms}?
   \<close>}
 
   \<^descr> @{method (HOL) meson} implements Loveland's model elimination
@@ -2170,8 +2170,8 @@
 
   @{rail \<open>
     @@{method (HOL) algebra}
-      ('add' ':' @{syntax thmrefs})?
-      ('del' ':' @{syntax thmrefs})?
+      ('add' ':' @{syntax thms})?
+      ('del' ':' @{syntax thms})?
     ;
     @@{attribute (HOL) algebra} (() | 'add' | 'del')
   \<close>}
@@ -2246,7 +2246,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method (HOL) coherent} @{syntax thmrefs}?
+    @@{method (HOL) coherent} @{syntax thms}?
   \<close>}
 
   \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent
@@ -2279,7 +2279,7 @@
     ;
     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
     ;
-    rule: 'rule' ':' @{syntax thmref}
+    rule: 'rule' ':' @{syntax thm}
   \<close>}
 
   \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
@@ -2379,9 +2379,9 @@
     ;
     constexpr: ( const | 'name._' | '_' )
     ;
-    typeconstructor: @{syntax nameref}
+    typeconstructor: @{syntax name}
     ;
-    class: @{syntax nameref}
+    class: @{syntax name}
     ;
     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -53,9 +53,9 @@
     ;
     @@{command prop} @{syntax modes}? @{syntax prop}
     ;
-    @@{command thm} @{syntax modes}? @{syntax thmrefs}
+    @@{command thm} @{syntax modes}? @{syntax thms}
     ;
-    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
+    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thms}?
     ;
     @@{command print_state} @{syntax modes}?
     ;
@@ -504,12 +504,12 @@
 
   @{rail \<open>
     (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
-      (@{syntax nameref} @{syntax mixfix} + @'and')
+      (@{syntax name} @{syntax mixfix} + @'and')
     ;
     (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
-      (@{syntax nameref} @{syntax mixfix} + @'and')
+      (@{syntax name} @{syntax mixfix} + @'and')
     ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
+    @@{command write} @{syntax mode}? (@{syntax name} @{syntax mixfix} + @'and')
   \<close>}
 
   \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
@@ -1103,7 +1103,7 @@
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
-    transpat: ('(' @{syntax nameref} ')')? @{syntax string}
+    transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>}
 
   \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -179,19 +179,14 @@
 
 text \<open>
   Entity @{syntax name} usually refers to any name of types, constants,
-  theorems etc.\ that are to be \<^emph>\<open>declared\<close> or \<^emph>\<open>defined\<close> (so qualified
-  identifiers are excluded here). Quoted strings provide an escape for
-  non-identifier names or those ruled out by outer syntax keywords (e.g.\
-  quoted \<^verbatim>\<open>"let"\<close>). Already existing objects are usually referenced by
-  @{syntax nameref}.
+  theorems etc.\ Quoted strings provide an escape for non-identifier names or
+  those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
 
   @{rail \<open>
-    @{syntax_def name}: @{syntax ident} | @{syntax symident} |
-      @{syntax string} | @{syntax nat}
+    @{syntax_def name}: @{syntax ident} | @{syntax longident} |
+      @{syntax symident} | @{syntax string} | @{syntax nat}
     ;
     @{syntax_def par_name}: '(' @{syntax name} ')'
-    ;
-    @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   \<close>}
 \<close>
 
@@ -219,13 +214,13 @@
 text \<open>
   Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
   i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
-  convenience, any of the smaller text units conforming to @{syntax nameref}
-  are admitted as well. A marginal @{syntax comment} is of the form
-  \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
-  within Isabelle/Isar commands.
+  convenience, any of the smaller text units conforming to @{syntax name} are
+  admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
+  text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
+  Isabelle/Isar commands.
 
   @{rail \<open>
-    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
+    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
     ;
     @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
   \<close>}
@@ -241,9 +236,9 @@
   directly at the outer level.
 
   @{rail \<open>
-    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
+    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax name} + ','))?
     ;
-    @{syntax_def sort}: @{syntax nameref}
+    @{syntax_def sort}: @{syntax name}
     ;
     @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
   \<close>}
@@ -265,10 +260,10 @@
   as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
 
   @{rail \<open>
-    @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
+    @{syntax_def type}: @{syntax name} | @{syntax typefree} |
       @{syntax typevar}
     ;
-    @{syntax_def term}: @{syntax nameref} | @{syntax var}
+    @{syntax_def term}: @{syntax name} | @{syntax var}
     ;
     @{syntax_def prop}: @{syntax term}
   \<close>}
@@ -377,7 +372,7 @@
   conforming to @{syntax symident}.
 
   @{rail \<open>
-    @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
+    @{syntax_def atom}: @{syntax name} | @{syntax typefree} |
       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
       @{syntax keyword} | @{syntax cartouche}
     ;
@@ -385,13 +380,13 @@
     ;
     @{syntax_def args}: arg *
     ;
-    @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
+    @{syntax_def attributes}: '[' (@{syntax name} @{syntax args} * ',') ']'
   \<close>}
 
   Theorem specifications come in several flavors: @{syntax axmdecl} and
   @{syntax thmdecl} usually refer to axioms, assumptions or results of goal
   statements, while @{syntax thmdef} collects lists of existing theorems.
-  Existing theorems are given by @{syntax thmref} and @{syntax thmrefs}, the
+  Existing theorems are given by @{syntax thm} and @{syntax thms}, the
   former requires an actual singleton result.
 
   There are three forms of theorem references:
@@ -426,12 +421,12 @@
     ;
     @{syntax_def thmdef}: thmbind '='
     ;
-    @{syntax_def thmref}:
-      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
+    @{syntax_def thm}:
+      (@{syntax name} selection? | @{syntax altstring} | @{syntax cartouche})
         @{syntax attributes}? |
       '[' @{syntax attributes} ']'
     ;
-    @{syntax_def thmrefs}: @{syntax thmref} +
+    @{syntax_def thms}: @{syntax thm} +
     ;
     selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
   \<close>}
@@ -465,13 +460,13 @@
     ;
     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
     ;
-    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+    thm_criterion: ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
     ;
     @@{command find_consts} (const_criterion*)
     ;
     const_criterion: ('-'?)
-      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
+      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
     ;
     @@{command thm_deps} @{syntax thmrefs}
     ;
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -283,10 +283,10 @@
   claim.
 
   @{rail \<open>
-    @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')
     ;
     (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
-      (@{syntax thmrefs} + @'and')
+      (@{syntax thms} + @'and')
   \<close>}
 
   \<^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>,
@@ -386,7 +386,7 @@
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
       stmt cond_stmt @{syntax for_fixes}
     ;
-    @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
+    @@{command print_statement} @{syntax modes}? @{syntax thms}
     ;
 
     stmt: (@{syntax props} + @'and')
@@ -513,7 +513,7 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
+    (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?
     ;
     @@{attribute trans} (() | 'add' | 'del')
   \<close>}
@@ -571,16 +571,16 @@
   ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
   once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
   proof methods are usually just a comma separated list of @{syntax
-  nameref}~@{syntax args} specifications. Note that parentheses may be dropped
+  name}~@{syntax args} specifications. Note that parentheses may be dropped
   for single method specifications (with no arguments). The syntactic
   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
   to high).
 
   @{rail \<open>
     @{syntax_def method}:
-      (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
+      (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
     ;
-    methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
+    methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   \<close>}
 
   Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
@@ -753,19 +753,19 @@
   @{rail \<open>
     @@{method goal_cases} (@{syntax name}*)
     ;
-    @@{method fact} @{syntax thmrefs}?
+    @@{method fact} @{syntax thms}?
     ;
-    @@{method (Pure) rule} @{syntax thmrefs}?
+    @@{method (Pure) rule} @{syntax thms}?
     ;
     rulemod: ('intro' | 'elim' | 'dest')
-      ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
+      ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}
     ;
     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
       ('!' | () | '?') @{syntax nat}?
     ;
     @@{attribute (Pure) rule} 'del'
     ;
-    @@{attribute OF} @{syntax thmrefs}
+    @@{attribute OF} @{syntax thms}
     ;
     @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
     ;
@@ -968,7 +968,7 @@
   advanced case analysis later.
 
   @{rail \<open>
-    @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
+    @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')
     ;
     @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
     ;
@@ -1076,7 +1076,7 @@
     @@{method coinduct} @{syntax insts} taking rule?
     ;
 
-    rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
+    rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)
     ;
     definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
     ;
@@ -1253,7 +1253,7 @@
     @@{attribute coinduct} spec
     ;
 
-    spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
+    spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'
   \<close>}
 
   \<^descr> @{command "print_induct_rules"} prints cases and induct rules for
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -37,7 +37,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    @@{command supply} (@{syntax thmdef}? @{syntax thms} + @'and')
     ;
     ( @@{command apply} | @@{command apply_end} ) @{syntax method}
     ;
@@ -222,7 +222,7 @@
   @{rail \<open>
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
-    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
+    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thm} | @{syntax thms} )
     ;
     @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
     ;
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -137,11 +137,11 @@
   \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.
 
   @{rail \<open>
-    @@{command context} @{syntax nameref} @'begin'
+    @@{command context} @{syntax name} @'begin'
     ;
     @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
     ;
-    @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
+    @{syntax_def target}: '(' @'in' @{syntax name} ')'
   \<close>}
 
   \<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing
@@ -226,13 +226,13 @@
   (\secref{sec:locale}).
 
   @{rail \<open>
-    @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
+    @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
     ;
     @@{command print_bundles} ('!'?)
     ;
-    (@@{command include} | @@{command including}) (@{syntax nameref}+)
+    (@@{command include} | @@{command including}) (@{syntax name}+)
     ;
-    @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
+    @{syntax_def "includes"}: @'includes' (@{syntax name}+)
   \<close>}
 
   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -383,7 +383,7 @@
     (@@{command declaration} | @@{command syntax_declaration})
       ('(' @'pervasive' ')')? \<newline> @{syntax text}
     ;
-    @@{command declare} (@{syntax thmrefs} + @'and')
+    @@{command declare} (@{syntax thms} + @'and')
   \<close>}
 
   \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type @{ML_type
@@ -440,7 +440,7 @@
   @{rail \<open>
     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     ;
-    instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
+    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
     ;
     qualifier: @{syntax name} ('?')?
     ;
@@ -490,7 +490,7 @@
     ;
     @@{command experiment} (@{syntax context_elem}*) @'begin'
     ;
-    @@{command print_locale} '!'? @{syntax nameref}
+    @@{command print_locale} '!'? @{syntax name}
     ;
     @@{command print_locales} ('!'?)
     ;
@@ -502,7 +502,7 @@
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
-      @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+      @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
   \<close>}
 
   \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
@@ -628,12 +628,12 @@
     @@{command global_interpretation} @{syntax locale_expr} \<newline>
       definitions? equations?
     ;
-    @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
+    @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
       definitions? equations?
     ;
     @@{command print_dependencies} '!'? @{syntax locale_expr}
     ;
-    @@{command print_interps} @{syntax nameref}
+    @@{command print_interps} @{syntax name}
     ;
 
     definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
@@ -798,15 +798,15 @@
     @@{command class} class_spec @'begin'?
     ;
     class_spec: @{syntax name} '='
-      ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
-        @{syntax nameref} | (@{syntax context_elem}+))      
+      ((@{syntax name} '+' (@{syntax context_elem}+)) |
+        @{syntax name} | (@{syntax context_elem}+))
     ;
-    @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
+    @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
     ;
-    @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
-      @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
+    @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |
+      @{syntax name} ('<' | '\<subseteq>') @{syntax name} )
     ;
-    @@{command subclass} @{syntax nameref}
+    @@{command subclass} @{syntax name}
     ;
     @@{command class_deps} (class_bounds class_bounds?)?
     ;
@@ -1054,7 +1054,7 @@
       @@{command SML_file_no_debug} |
       @@{command ML_file} |
       @@{command ML_file_debug} |
-      @@{command ML_file_no_debug}) @{syntax xname} ';'?
+      @@{command ML_file_no_debug}) @{syntax name} ';'?
     ;
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
@@ -1231,7 +1231,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command lemmas} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')
       @{syntax for_fixes}
     ;
     @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
@@ -1299,7 +1299,7 @@
 
   @{rail \<open>
     ( @{command hide_class} | @{command hide_type} |
-      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
+      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
   \<close>}
 
   Isabelle organizes any kind of name declarations (of types, constants,
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -1068,7 +1068,7 @@
   single criterium has the following syntax:
 
   @{rail \<open>
-    ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+    ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
   \<close>}
 
@@ -1086,7 +1086,7 @@
 
   @{rail \<open>
     ('-'?)
-      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
+      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
   \<close>}
 
   See also the Isar command @{command_ref find_consts} in @{cite
diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Logics_ZF/ZF_Isar.thy
--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -69,13 +69,13 @@
     hints: @{syntax (ZF) "monos"}? condefs? \<newline>
       @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
     ;
-    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
+    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thms}
     ;
-    condefs: @'con_defs' @{syntax thmrefs}
+    condefs: @'con_defs' @{syntax thms}
     ;
-    @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
+    @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thms}
     ;
-    @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
+    @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thms}
   \<close>}
 
   In the following syntax specification @{text "monos"}, @{text
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -244,7 +244,7 @@
   end |> Pretty.writeln;
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Library/rewrite.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -442,7 +442,7 @@
     val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
 
     val subst_parser =
-      let val scan = raw_pattern -- to_parser -- Parse.xthms1
+      let val scan = raw_pattern -- to_parser -- Parse.thms1
       in context_lift scan prep_args end
   in
     Method.setup @{binding rewrite} (subst_parser >>
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -231,15 +231,15 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword case_of_simps}
     "turn a list of equations into a case expression"
-    (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
+    (Parse_Spec.opt_thm_name ":"  -- Parse.thms1 >> case_of_simps_cmd)
 
 val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
-  Parse.xthms1 --| @{keyword ")"}
+  Parse.thms1 --| @{keyword ")"}
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword simps_of_case}
     "perform case split on rule"
-    (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
+    (Parse_Spec.opt_thm_name ":"  -- Parse.thm --
       Scan.optional parse_splits [] >> simps_of_case_cmd)
 
 end
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -536,7 +536,7 @@
       let
         val ref_of_str = (* FIXME proper wrapper for parser combinators *)
           suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
-          #> Parse.xthm #> fst
+          #> Parse.thm #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
         val fact_override = {add = facts, del = [], only = true}
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -680,14 +680,14 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
-    (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
+    (Parse.name -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
       (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
         prove_strong_ind name avoids));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword equivariance}
     "prove equivariance for inductive predicate involving nominal datatypes"
-    (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
+    (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
       (fn (name, atoms) => prove_eqvt name atoms));
 
 end
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -488,7 +488,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
     "prove strong induction theorem for inductive predicate involving nominal datatypes"
-    (Parse.xname -- 
+    (Parse.name -- 
      Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
      (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
       (@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/SPARK/Manual/Reference.thy
--- a/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -51,7 +51,7 @@
 @{rail \<open>
   @'spark_types' ((name '=' type (mapping?))+)
   ;
-  mapping: '('((name '=' nameref)+',')')'
+  mapping: '('((name '=' name)+',')')'
 \<close>}
 Associates a \SPARK{} type with the given name with an Isabelle type. This command can
 only be used outside a verification environment. The given type must be either a record
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -117,7 +117,7 @@
     "associate SPARK types with types"
     (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
        Scan.optional (Args.parens (Parse.list1
-         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
+         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >>
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -642,7 +642,7 @@
 
 val parent =
   Parse_Spec.locale_prefix --
-  ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
+  ((type_insts -- Parse.name) || (Parse.name >> pair [])) -- renames
     >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
 
 in
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -426,7 +426,7 @@
   Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
     (K Plugin_Name.default_filter) >> Plugins_Option >> single;
 
-val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.xthm);
+val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
 
 in
 
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -305,7 +305,7 @@
 val add_partial_function = gen_add_partial_function Specification.check_spec;
 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
 
-val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
+val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -812,7 +812,7 @@
       (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
           >> Scan.triple2) --
         (@{keyword "is"} |-- Parse.term) --
-        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Scan.triple1)
+        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.thms1) []) >> Scan.triple1)
      >> lift_def_cmd_with_err_handling);
 
 end
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -809,8 +809,8 @@
 val _ = 
   Outer_Syntax.local_theory @{command_keyword setup_lifting}
     "setup lifting infrastructure" 
-      (Parse.xthm -- Scan.option Parse.xthm 
-      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
+      (Parse.thm -- Scan.option Parse.thm 
+      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm) >> 
         (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
           setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
 
@@ -1024,7 +1024,7 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword lifting_forget} 
     "unsetup Lifting and Transfer for the given lifting bundle"
-    (Parse.position Parse.xname >> (lifting_forget_cmd))
+    (Parse.position Parse.name >> (lifting_forget_cmd))
 
 (* lifting_update *)
 
@@ -1053,6 +1053,6 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword lifting_update}
     "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
-    (Parse.position Parse.xname >> lifting_update_cmd)
+    (Parse.position Parse.name >> lifting_update_cmd)
 
 end
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -1030,7 +1030,7 @@
 (* values command for Prolog queries *)
 
 val opt_print_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
 
 val _ =
   Outer_Syntax.command @{command_keyword values_prolog}
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -222,12 +222,12 @@
     parse_mode_tuple_expr) xs
 
 val mode_and_opt_proposal = parse_mode_expr --
-  Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
+  Scan.optional (Args.$$$ "as" |-- Parse.name >> SOME) NONE
 
 
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
-    (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
+    (((Parse.enum1 "and" (Parse.name --| @{keyword ":"} --
         (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
       || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
     --| @{keyword ")"}) (Multiple_Preds [])
@@ -250,7 +250,7 @@
   end
 
 val opt_print_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
 
 val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
 
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -348,7 +348,7 @@
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
           Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
-        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm))
       >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
 
 end
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -349,10 +349,10 @@
 
 val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
 val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
-val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
+val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
-val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.xthm)
+val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
 val parse_fact_override_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -129,7 +129,7 @@
     |> Symbol.source
     |> Token.source keywords Position.start
     |> Token.source_proper
-    |> Source.source Token.stopper (Parse.xthms1 >> get)
+    |> Source.source Token.stopper (Parse.thms1 >> get)
     |> Source.exhaust
   end
 
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -1182,7 +1182,7 @@
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_alt_specs [] --
-  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd o gen_add_inductive mk_def true coind preds params specs monos));
 
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/record.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -2411,7 +2411,7 @@
         Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
 
 val _ =
   Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -166,7 +166,7 @@
   implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
 
 val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm));
 
 val parse_attr =
   Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/value.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -64,10 +64,10 @@
   in Pretty.writeln p end;
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
 
 val opt_evaluator =
-  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
   
 val _ =
   Outer_Syntax.command @{command_keyword value} "evaluate and print term"
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -209,7 +209,7 @@
           val description = List(xname1, "(" + descr_name + ")")
           val replacement =
             Token.explode(Keyword.Keywords.empty, xname1) match {
-              case List(tok) if tok.is_xname => xname1
+              case List(tok) if tok.is_name => xname1
               case _ => quote(xname1)
             }
           Item(range, original, full_name, description, replacement, 0, true)
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -599,7 +599,7 @@
 local
 
 fun sect (modifier : modifier parser) = Scan.depend (fn context =>
-  Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.xthm)
+  Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.thm)
     >> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) =>
       let
         val decl =
@@ -689,7 +689,7 @@
 
 fun parser pri =
   let
-    val meth_name = Parse.token Parse.xname;
+    val meth_name = Parse.token Parse.name;
 
     fun meth5 x =
      (meth_name >> (Source o single) ||
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -64,12 +64,10 @@
   val properties: Properties.T parser
   val name: bstring parser
   val binding: binding parser
-  val xname: xstring parser
   val text: string parser
   val path: string parser
-  val theory_name: bstring parser
-  val theory_xname: xstring parser
-  val liberal_name: xstring parser
+  val theory_name: string parser
+  val liberal_name: string parser
   val parname: string parser
   val parbinding: binding parser
   val class: string parser
@@ -104,15 +102,15 @@
   val termp: (string * string list) parser
   val private: Position.T parser
   val qualified: Position.T parser
-  val target: (xstring * Position.T) parser
-  val opt_target: (xstring * Position.T) option parser
+  val target: (string * Position.T) parser
+  val opt_target: (string * Position.T) option parser
   val args: Token.T list parser
   val args1: (string -> bool) -> Token.T list parser
   val attribs: Token.src list parser
   val opt_attribs: Token.src list parser
   val thm_sel: Facts.interval list parser
-  val xthm: (Facts.ref * Token.src list) parser
-  val xthms1: (Facts.ref * Token.src list) list parser
+  val thm: (Facts.ref * Token.src list) parser
+  val thms1: (Facts.ref * Token.src list) list parser
 end;
 
 structure Parse: PARSE =
@@ -261,22 +259,20 @@
 
 (* names and text *)
 
-val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
+val name =
+  group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
 
 val binding = position name >> Binding.make;
 
-val xname = group (fn () => "name reference")
-  (short_ident || long_ident || sym_ident || string || number);
+val text =
+  group (fn () => "text")
+    (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
 
-val text = group (fn () => "text")
-  (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
-
-val path = group (fn () => "file name/path specification") xname;
+val path = group (fn () => "file name/path specification") name;
 
 val theory_name = group (fn () => "theory name") name;
-val theory_xname = group (fn () => "theory name reference") xname;
 
-val liberal_name = keyword_with Token.ident_or_symbolic || xname;
+val liberal_name = keyword_with Token.ident_or_symbolic || name;
 
 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
 val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
@@ -284,11 +280,11 @@
 
 (* type classes *)
 
-val class = group (fn () => "type class") (inner_syntax xname);
+val class = group (fn () => "type class") (inner_syntax name);
 
-val sort = group (fn () => "sort") (inner_syntax xname);
+val sort = group (fn () => "sort") (inner_syntax name);
 
-val type_const = inner_syntax (group (fn () => "type constructor") xname);
+val type_const = inner_syntax (group (fn () => "type constructor") name);
 
 val arity = type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
@@ -398,7 +394,7 @@
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
-val const = inner_syntax (group (fn () => "constant") xname);
+val const = inner_syntax (group (fn () => "constant") name);
 
 val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
 
@@ -417,7 +413,7 @@
 val private = position ($$$ "private") >> #2;
 val qualified = position ($$$ "qualified") >> #2;
 
-val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
+val target = ($$$ "(" -- $$$ "in") |-- !!! (position name --| $$$ ")");
 val opt_target = Scan.option target;
 
 
@@ -468,11 +464,11 @@
   nat --| minus >> Facts.From ||
   nat >> Facts.Single) --| $$$ ")";
 
-val xthm =
+val thm =
   $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
   (literal_fact >> Facts.Fact ||
-    position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+    position name -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
 
-val xthms1 = Scan.repeat1 xthm;
+val thms1 = Scan.repeat1 thm;
 
 end;
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/parse.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -67,19 +67,16 @@
 
     def string: Parser[String] = atom("string", _.is_string)
     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
-    def name: Parser[String] = atom("name declaration", _.is_name)
-    def xname: Parser[String] = atom("name reference", _.is_xname)
+    def name: Parser[String] = atom("name", _.is_name)
     def text: Parser[String] = atom("text", _.is_text)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
 
     def path: Parser[String] =
-      atom("file name/path specification", tok => tok.is_xname && Path.is_wellformed(tok.content))
+      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
 
     def theory_name: Parser[String] =
       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
-    def theory_xname: Parser[String] =
-      atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content))
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -55,7 +55,7 @@
 
 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
 
-val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1);
 
 
 (* basic constant specifications *)
@@ -72,7 +72,7 @@
 
 (* locale and context elements *)
 
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name));
 
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
@@ -95,7 +95,7 @@
     >> Element.Assumes ||
   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
     >> Element.Defines ||
-  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1))
+  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.thms1))
     >> (curry Element.Notes "");
 
 fun plus1_unless test scan =
@@ -120,7 +120,7 @@
 
 val locale_expression =
   let
-    val expr2 = Parse.position Parse.xname;
+    val expr2 = Parse.position Parse.name;
     val expr1 =
       locale_prefix -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/token.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -38,7 +38,6 @@
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
   val is_command: T -> bool
-  val is_name: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
@@ -210,8 +209,6 @@
 
 val is_command = is_kind Command;
 
-val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
-
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Isar/token.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -236,11 +236,11 @@
   def is_float: Boolean = kind == Token.Kind.FLOAT
   def is_name: Boolean =
     kind == Token.Kind.IDENT ||
+    kind == Token.Kind.LONG_IDENT ||
     kind == Token.Kind.SYM_IDENT ||
     kind == Token.Kind.STRING ||
     kind == Token.Kind.NAT
-  def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
-  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
+  def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_improper: Boolean = is_space || is_comment
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -96,7 +96,7 @@
 local
 
 val antiq =
-  Parse.!!! ((Parse.token Parse.xname ::: Parse.args) --| Scan.ahead Parse.eof);
+  Parse.!!! ((Parse.token Parse.name ::: Parse.args) --| Scan.ahead Parse.eof);
 
 fun make_env name visible =
   (ML_Lex.tokenize
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -322,7 +322,7 @@
   private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
     if (tokens.exists({ case (t, _) => t.is_command })) {
       tokens.dropWhile({ case (t, _) => !t.is_command }).
-        collectFirst({ case (t, i) if t.is_xname => (t.content, i) })
+        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
     }
     else None
 
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Pure.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -280,7 +280,7 @@
 
 val trans_pat =
   Scan.optional
-    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
+    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
@@ -403,7 +403,7 @@
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
-    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
+    (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
@@ -442,7 +442,7 @@
 
 val _ =
   hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
-    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
+    (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
 
 in end\<close>
 
@@ -454,18 +454,18 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
-    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword include}
     "include declarations from bundle in proof body"
-    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
+    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword including}
     "include declarations from bundle in goal refinement"
-    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
+    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_bundles}
@@ -484,7 +484,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword context} "begin local theory context"
-    ((Parse.position Parse.xname >> (fn name =>
+    ((Parse.position Parse.name >> (fn name =>
         Toplevel.begin_local_theory true (Named_Target.begin name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
@@ -550,7 +550,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
-    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
+    ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
     || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
@@ -684,7 +684,7 @@
 ML \<open>
 local
 
-val facts = Parse.and_list1 Parse.xthms1;
+val facts = Parse.and_list1 Parse.thms1;
 
 val _ =
   Outer_Syntax.command @{command_keyword then} "forward chaining"
@@ -773,9 +773,9 @@
   Outer_Syntax.command @{command_keyword case} "invoke local context"
     (Parse_Spec.opt_thm_name ":" --
       (@{keyword "("} |--
-        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+        Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
           --| @{keyword ")"}) ||
-        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
+        Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
 
 in end\<close>
 
@@ -906,7 +906,7 @@
 local
 
 val calculation_args =
-  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
 
 val _ =
   Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
@@ -956,7 +956,7 @@
 local
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword help}
@@ -1025,13 +1025,13 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_locale}
     "print locale of this theory"
-    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
+    (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_interps}
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.xname >> (fn name =>
+    (Parse.position Parse.name >> (fn name =>
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
@@ -1100,19 +1100,19 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_statement}
     "print theorems as long statements"
-    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
+    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.command @{command_keyword thm} "print theorems"
-    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
+    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
-    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
+    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
-    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
+    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.command @{command_keyword prop} "read and print proposition"
@@ -1156,8 +1156,8 @@
 local
 
 val theory_bounds =
-  Parse.position Parse.theory_xname >> single ||
-  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
+  Parse.position Parse.theory_name >> single ||
+  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
 
 val _ =
   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
@@ -1177,14 +1177,14 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
-    (Parse.xthms1 >> (fn args =>
+    (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
         Thm_Deps.thm_deps (Toplevel.theory_of st)
           (Attrib.eval_thms (Toplevel.context_of st) args))));
 
 
 val thy_names =
-  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
+  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
 
 val _ =
   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
@@ -1260,7 +1260,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword realizers}
     "specify realizers for primitive axioms / theorems, together with correctness proof"
-    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
+    (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
@@ -1276,7 +1276,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
-    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+    (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 
 in end\<close>
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -201,7 +201,7 @@
 
       val theories =
         ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
-          ((options | success(Nil)) ~ rep(theory_xname)) ^^
+          ((options | success(Nil)) ~ rep(theory_name)) ^^
           { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
 
       val document_files =
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/term_style.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -32,7 +32,7 @@
 (* style parsing *)
 
 fun parse_single ctxt =
-  Parse.token Parse.xname ::: Parse.args >> (fn src0 =>
+  Parse.token Parse.name ::: Parse.args >> (fn src0 =>
     let
       val (src, parse) = Token.check_src ctxt get_data src0;
       val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -117,7 +117,7 @@
 
 fun imports name =
   if name = Context.PureN then Scan.succeed []
-  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
+  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
 
 val opt_files =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 13 18:01:05 2016 +0200
@@ -109,7 +109,7 @@
 
     val args =
       position(theory_name) ~
-      (opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^
+      (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -143,7 +143,7 @@
 local
 
 val property =
-  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
+  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
 
 val properties =
   Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
@@ -404,7 +404,7 @@
 
 val locale =
   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
-    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
+    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
 in
 
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -136,7 +136,7 @@
 local
 
 val criterion =
-  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
   Parse.typ >> Loose;
 
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -509,7 +509,7 @@
 local
 
 val criterion =
-  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
   Parse.reserved "intro" >> K Intro ||
   Parse.reserved "elim" >> K Elim ||
   Parse.reserved "dest" >> K Dest ||
diff -r 4e4738698db4 -r 9f394a16c557 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -104,7 +104,7 @@
 fun read_inst ctxt (raw_tyco, raw_class) =
   (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
 
-val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
+val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class;
 
 fun cert_syms ctxt =
   Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
diff -r 4e4738698db4 -r 9f394a16c557 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -433,9 +433,9 @@
     ("define " ^ coind_prefix ^ "datatype")
     ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
       Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
-      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
-      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
-      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
+      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
+      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
+      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
       >> (Toplevel.theory o mk_datatype));
 
 end;
diff -r 4e4738698db4 -r 9f394a16c557 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -192,10 +192,10 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
-    ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
-     (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
-     (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
-     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.xthms1) []
+    ((@{keyword "elimination"} |-- Parse.!!! Parse.thm) --
+     (@{keyword "induction"} |-- Parse.!!! Parse.thm) --
+     (@{keyword "case_eqns"} |-- Parse.!!! Parse.thms1) --
+     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.thms1) []
      >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
 
 end;
diff -r 4e4738698db4 -r 9f394a16c557 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -587,10 +587,10 @@
       ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
   (@{keyword "intros"} |--
     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
-  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
-  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.xthms1) [] --
-  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
-  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
+  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.thms1) [] --
+  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
+  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
   >> (Toplevel.theory o mk_ind);
 
 val _ =