1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 17 17:58:40 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 17 22:46:19 2012 +0100
     1.3 @@ -103,10 +103,10 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail "
     1.7 -    @@{command context} @{syntax name} @'begin'
     1.8 +    @@{command context} @{syntax nameref} @'begin'
     1.9      ;
    1.10  
    1.11 -    @{syntax_def target}: '(' @'in' @{syntax name} ')'
    1.12 +    @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
    1.13    "}
    1.14  
    1.15    \begin{description}

     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 17:58:40 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 22:46:19 2012 +0100
     2.3 @@ -148,13 +148,13 @@
     2.4    \begin{railoutput}
     2.5  \rail@begin{1}{}
     2.6  \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
     2.7 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
     2.8 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
     2.9  \rail@term{\isa{\isakeyword{begin}}}[]
    2.10  \rail@end
    2.11  \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
    2.12  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    2.13  \rail@term{\isa{\isakeyword{in}}}[]
    2.14 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    2.15 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
    2.16  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    2.17  \rail@end
    2.18  \end{railoutput}

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 17 17:58:40 2012 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 17 22:46:19 2012 +0100
     3.3 @@ -410,7 +410,7 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
     3.7 -    (Parse.position Parse.name --| Parse.begin >> (fn name =>
     3.8 +    (Parse.position Parse.xname --| Parse.begin >> (fn name =>
     3.9        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
    3.10  
    3.11