# HG changeset patch
# User wenzelm
# Date 1332020779 -3600
# Node ID 1c3c185bab4e22080585c2c906bac9b7421f026a
# Parent  11b38c94b21ab5e98442b0cf96e631a649cac44a
more precise syntax;

diff -r 11b38c94b21a -r 1c3c185bab4e doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 17 17:58:40 2012 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 17 22:46:19 2012 +0100
@@ -103,10 +103,10 @@
   \end{matharray}
 
   @{rail "
-    @@{command context} @{syntax name} @'begin'
+    @@{command context} @{syntax nameref} @'begin'
     ;
 
-    @{syntax_def target}: '(' @'in' @{syntax name} ')'
+    @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
   "}
 
   \begin{description}
diff -r 11b38c94b21a -r 1c3c185bab4e doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 17:58:40 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 22:46:19 2012 +0100
@@ -148,13 +148,13 @@
   \begin{railoutput}
 \rail@begin{1}{}
 \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
 \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@term{\isa{\isakeyword{in}}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
 \end{railoutput}
diff -r 11b38c94b21a -r 1c3c185bab4e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 17 17:58:40 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 17 22:46:19 2012 +0100
@@ -410,7 +410,7 @@
 
 val _ =
   Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
-    (Parse.position Parse.name --| Parse.begin >> (fn name =>
+    (Parse.position Parse.xname --| Parse.begin >> (fn name =>
       Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));