--- 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