src/Doc/Isar_Ref/Spec.thy

     @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{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'?
     ;
     @@{command experiment} (@{syntax context_elem}*) @'begin'
     ;