# HG changeset patch
# User wenzelm
# Date 1621792777 -7200
# Node ID 1419cb7f7f3eec5356871481112d1b41cc7eb1db
# Parent  08db0a06e13108cf08f4f2b718739b192a6d8213
clarified index, more like formal @{element_ref};

diff -r 08db0a06e131 -r 1419cb7f7f3e src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sun May 23 19:29:18 2021 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun May 23 19:59:37 2021 +0200
@@ -520,11 +520,11 @@
     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   \end{tabular}
 
-  @{index_ref \<open>\<^theory_text>\<open>fixes\<close>\<close>}
-  @{index_ref \<open>\<^theory_text>\<open>constrains\<close>\<close>}
-  @{index_ref \<open>\<^theory_text>\<open>assumes\<close>\<close>}
-  @{index_ref \<open>\<^theory_text>\<open>defines\<close>\<close>}
-  @{index_ref \<open>\<^theory_text>\<open>notes\<close>\<close>}
+  @{index_ref \<open>\<^theory_text>\<open>fixes\<close> (element)\<close>}
+  @{index_ref \<open>\<^theory_text>\<open>constrains\<close> (element)\<close>}
+  @{index_ref \<open>\<^theory_text>\<open>assumes\<close> (element)\<close>}
+  @{index_ref \<open>\<^theory_text>\<open>defines\<close> (element)\<close>}
+  @{index_ref \<open>\<^theory_text>\<open>notes\<close> (element)\<close>}
   \<^rail>\<open>
     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
     ;