src/Doc/JEdit/JEdit.thy
changeset 62969 9f394a16c557
parent 62917 eed66ba99bd9
child 63669 256fc20716f2
--- 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