# HG changeset patch
# User wenzelm
# Date 1330028111 -3600
# Node ID e1bdcbe04b8383269ce1d974bcffc45bcf7dec23
# Parent  fbe2cb05bdb39fce3018f739b1ec586ab508ec52
prefer actual syntax categories;

diff -r fbe2cb05bdb3 -r e1bdcbe04b83 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Feb 23 20:40:20 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Feb 23 21:15:11 2012 +0100
@@ -1648,7 +1648,7 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
+    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     ;
 
     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -1662,11 +1662,11 @@
       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
     ;
 
-    @@{command (HOL) quickcheck_generator} typeconstructor \\
+    @@{command (HOL) quickcheck_generator} @{syntax nameref} \\
       'operations:' ( @{syntax term} +)
     ;
 
-    @@{command (HOL) find_unused_assms} theoryname?
+    @@{command (HOL) find_unused_assms} @{syntax name}?
     ;
 
     modes: '(' (@{syntax name} +) ')'
diff -r fbe2cb05bdb3 -r e1bdcbe04b83 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Feb 23 20:40:20 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Feb 23 21:15:11 2012 +0100
@@ -2351,7 +2351,7 @@
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
-\rail@nont{\isa{name}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
 \rail@endbar
 \rail@bar
@@ -2408,7 +2408,7 @@
 \rail@end
 \rail@begin{4}{}
 \rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
-\rail@nont{\isa{typeconstructor}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@cr{2}
 \rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
 \rail@plus
@@ -2420,7 +2420,7 @@
 \rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\isa{theoryname}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@endbar
 \rail@end
 \rail@begin{2}{\isa{modes}}