doc-src/Ref/ref.ind

     \subitem of macros, 94, 95
     \subitem of mixfix declarations, 77
     \subitem of simplification, 117
     \subitem of translations, 98
   \item exceptions
-    \subitem printing of, 5
+    \subitem printing of, 6
   \item {\tt exit}, \bold{2}
   \item {\tt extensional}, \bold{48}
 
   \indexspace
 

   \item {\tt loadpath}, \bold{58}
   \item {\tt logic} class, 72, 77
   \item {\tt logic} nonterminal, \bold{72}
   \item {\tt Logic.auto_rename}, \bold{25}
   \item {\tt Logic.set_rename_prefix}, \bold{24}
-  \item {\tt long_names}, \bold{4}
+  \item {\tt long_names}, \bold{5}
   \item {\tt loose_bnos}, \bold{63}, 99
 
   \indexspace
 
   \item macros, 90--96

   \item {\tt parents_of}, \bold{61}
   \item parse trees, 85
   \item {\tt parse_rules}, 92
   \item pattern, higher-order, \bold{110}
   \item {\tt pause_tac}, \bold{29}
-  \item Poly/{\ML} compiler, 5
+  \item Poly/{\ML} compiler, 6
   \item {\tt pop_proof}, \bold{16}
   \item {\tt pr}, \bold{12}
   \item {\tt premises}, \bold{8}, 16
   \item {\tt prems_of}, \bold{44}
   \item {\tt prems_of_ss}, \bold{113}

     \subitem theory, 56
   \item shortcuts
     \subitem for \texttt{by} commands, 13
     \subitem for tactics, 22
   \item {\tt show_brackets}, \bold{4}
-  \item {\tt show_consts}, \bold{4}
+  \item {\tt show_consts}, \bold{5}
   \item {\tt show_hyps}, \bold{4}
   \item {\tt show_sorts}, \bold{4}, 89, 97
+  \item {\tt show_tags}, \bold{4}
   \item {\tt show_types}, \bold{4}, 89, 92, 99
   \item {\tt Sign.certify_term}, \bold{65}
   \item {\tt Sign.certify_typ}, \bold{66}
   \item {\tt Sign.sg} ML type, 54
   \item {\tt Sign.stamp_names_of}, \bold{62}