# HG changeset patch
# User wenzelm
# Date 1621540939 -7200
# Node ID cb933ba9ecfe484a58755ce81823b459f74cb9af
# Parent  f9c8da2539449766d561814e2ec192f495575b7b
tuned index;

diff -r f9c8da253944 -r cb933ba9ecfe src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu May 20 21:21:37 2021 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu May 20 22:02:19 2021 +0200
@@ -520,8 +520,11 @@
     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   \end{tabular}
 
-  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
-  \indexisarelem{defines}\indexisarelem{notes}
+  @{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>}
   \<^rail>\<open>
     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
     ;
diff -r f9c8da253944 -r cb933ba9ecfe src/Doc/isar.sty
--- a/src/Doc/isar.sty	Thu May 20 21:21:37 2021 +0200
+++ b/src/Doc/isar.sty	Thu May 20 22:02:19 2021 +0200
@@ -9,8 +9,6 @@
 \newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}}
 \newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}}
 
-\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
-
 \newcommand{\isasymIF}{\isakeyword{if}}
 \newcommand{\isasymFOR}{\isakeyword{for}}
 \newcommand{\isasymAND}{\isakeyword{and}}