# HG changeset patch
# User wenzelm
# Date 1621713133 -7200
# Node ID 35d8132633c65250e15c7ac080969500fc22db35
# Parent  eccc4a13216d1f6a73ca56c5935822257b02a650
clarified names;

diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Eq.thy	Sat May 22 21:52:13 2021 +0200
@@ -55,13 +55,13 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Thm.reflexive: "cterm -> thm"} \\
-  @{index_ML Thm.symmetric: "thm -> thm"} \\
-  @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
-  @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
-  @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
-  @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
-  @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
+  @{define_ML Thm.reflexive: "cterm -> thm"} \\
+  @{define_ML Thm.symmetric: "thm -> thm"} \\
+  @{define_ML Thm.transitive: "thm -> thm -> thm"} \\
+  @{define_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
+  @{define_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
+  @{define_ML Thm.equal_intr: "thm -> thm -> thm"} \\
+  @{define_ML Thm.equal_elim: "thm -> thm -> thm"} \\
   \end{mldecls}
 
   See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
@@ -82,9 +82,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_structure Conv} \\
-  @{index_ML_type conv} \\
-  @{index_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
+  @{define_ML_structure Conv} \\
+  @{define_ML_type conv} \\
+  @{define_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
   \end{mldecls}
 
   \<^descr> \<^ML_structure>\<open>Conv\<close> is a library of combinators to build conversions,
@@ -109,11 +109,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
-  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
+  @{define_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{define_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{define_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
+  @{define_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>rewrite_rule\<close>~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Integration.thy	Sat May 22 21:52:13 2021 +0200
@@ -37,11 +37,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Toplevel.state} \\
-  @{index_ML_exception Toplevel.UNDEF} \\
-  @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
-  @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
-  @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
+  @{define_ML_type Toplevel.state} \\
+  @{define_ML_exception Toplevel.UNDEF} \\
+  @{define_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
+  @{define_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
+  @{define_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Toplevel.state\<close> represents Isar toplevel states, which are
@@ -95,17 +95,17 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
+  @{define_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.theory: "(theory -> theory) ->
+  @{define_ML Toplevel.theory: "(theory -> theory) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
+  @{define_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
+  @{define_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
+  @{define_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
+  @{define_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
   Toplevel.transition -> Toplevel.transition"} \\
   \end{mldecls}
 
@@ -150,10 +150,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML use_thy: "string -> unit"} \\
-  @{index_ML Thy_Info.get_theory: "string -> theory"} \\
-  @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
-  @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
+  @{define_ML use_thy: "string -> unit"} \\
+  @{define_ML Thy_Info.get_theory: "string -> theory"} \\
+  @{define_ML Thy_Info.remove_thy: "string -> unit"} \\
+  @{define_ML Thy_Info.register_thy: "theory -> unit"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Isar.thy	Sat May 22 21:52:13 2021 +0200
@@ -60,16 +60,16 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Proof.state} \\
-  @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
-  @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
-  @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
-  @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
-  @{index_ML Proof.goal: "Proof.state ->
+  @{define_ML_type Proof.state} \\
+  @{define_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
+  @{define_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
+  @{define_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
+  @{define_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
+  @{define_ML Proof.goal: "Proof.state ->
   {context: Proof.context, facts: thm list, goal: thm}"} \\
-  @{index_ML Proof.raw_goal: "Proof.state ->
+  @{define_ML Proof.raw_goal: "Proof.state ->
   {context: Proof.context, facts: thm list, goal: thm}"} \\
-  @{index_ML Proof.theorem: "Method.text option ->
+  @{define_ML Proof.theorem: "Method.text option ->
   (thm list list -> Proof.context -> Proof.context) ->
   (term * term list) list list -> Proof.context -> Proof.state"} \\
   \end{mldecls}
@@ -272,13 +272,13 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Proof.method} \\
-  @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
-  @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
-  @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
-  @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
-  @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
+  @{define_ML_type Proof.method} \\
+  @{define_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
+  @{define_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
+  @{define_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
+  @{define_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
+  @{define_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
   string -> theory -> theory"} \\
   \end{mldecls}
 
@@ -286,7 +286,7 @@
 
   \<^descr> \<^ML>\<open>CONTEXT_METHOD\<close>~\<open>(fn facts => context_tactic)\<close> wraps \<open>context_tactic\<close>
   depending on goal facts as a general proof method that may change the proof
-  context dynamically. A typical operation is \<^ML>\<open>Proof_Context.update_cases\<close>, which is wrapped up as combinator @{index_ML
+  context dynamically. A typical operation is \<^ML>\<open>Proof_Context.update_cases\<close>, which is wrapped up as combinator @{define_ML
   CONTEXT_CASES} for convenience.
 
   \<^descr> \<^ML>\<open>METHOD\<close>~\<open>(fn facts => tactic)\<close> wraps \<open>tactic\<close> depending on goal facts
@@ -495,12 +495,12 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type attribute} \\
-  @{index_ML Thm.rule_attribute: "thm list ->
+  @{define_ML_type attribute} \\
+  @{define_ML Thm.rule_attribute: "thm list ->
   (Context.generic -> thm -> thm) -> attribute"} \\
-  @{index_ML Thm.declaration_attribute: "
+  @{define_ML Thm.declaration_attribute: "
   (thm -> Context.generic -> Context.generic) -> attribute"} \\
-  @{index_ML Attrib.setup: "binding -> attribute context_parser ->
+  @{define_ML Attrib.setup: "binding -> attribute context_parser ->
   string -> theory -> theory"} \\
   \end{mldecls}
 
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Sat May 22 21:52:13 2021 +0200
@@ -90,11 +90,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type local_theory = Proof.context} \\
-  @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
-  @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
+  @{define_ML_type local_theory = Proof.context} \\
+  @{define_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
+  @{define_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
-  @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
+  @{define_ML Local_Theory.note: "Attrib.binding * thm list ->
     local_theory -> (string * thm list) * local_theory"} \\
   \end{mldecls}
 
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat May 22 21:52:13 2021 +0200
@@ -102,22 +102,22 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type class = string} \\
-  @{index_ML_type sort = "class list"} \\
-  @{index_ML_type arity = "string * sort list * sort"} \\
-  @{index_ML_type typ} \\
-  @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
-  @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
+  @{define_ML_type class = string} \\
+  @{define_ML_type sort = "class list"} \\
+  @{define_ML_type arity = "string * sort list * sort"} \\
+  @{define_ML_type typ} \\
+  @{define_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
+  @{define_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
-  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
-  @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
-  @{index_ML Sign.add_type_abbrev: "Proof.context ->
+  @{define_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
+  @{define_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
+  @{define_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
+  @{define_ML Sign.add_type_abbrev: "Proof.context ->
   binding * string list * typ -> theory -> theory"} \\
-  @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
-  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
-  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
+  @{define_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
+  @{define_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
+  @{define_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>class\<close> represents type classes.
@@ -313,30 +313,30 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type term} \\
-  @{index_ML_infix "aconv": "term * term -> bool"} \\
-  @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
-  @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
-  @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
-  @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
+  @{define_ML_type term} \\
+  @{define_ML_infix "aconv": "term * term -> bool"} \\
+  @{define_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
+  @{define_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
+  @{define_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
+  @{define_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML fastype_of: "term -> typ"} \\
-  @{index_ML lambda: "term -> term -> term"} \\
-  @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML incr_boundvars: "int -> term -> term"} \\
-  @{index_ML Sign.declare_const: "Proof.context ->
+  @{define_ML fastype_of: "term -> typ"} \\
+  @{define_ML lambda: "term -> term -> term"} \\
+  @{define_ML betapply: "term * term -> term"} \\
+  @{define_ML incr_boundvars: "int -> term -> term"} \\
+  @{define_ML Sign.declare_const: "Proof.context ->
   (binding * typ) * mixfix -> theory -> term * theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> binding * term ->
+  @{define_ML Sign.add_abbrev: "string -> binding * term ->
   theory -> (term * term) * theory"} \\
-  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
-  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
+  @{define_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
+  @{define_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>term\<close> represents de-Bruijn terms, with comments in
   abstractions, and explicitly named free variables and constants; this is a
-  datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML
-  Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_infix "$"}.
+  datatype with constructors @{define_ML Bound}, @{define_ML Free}, @{define_ML
+  Var}, @{define_ML Const}, @{define_ML Abs}, @{define_ML_infix "$"}.
 
   \<^descr> \<open>t\<close>~\<^ML_text>\<open>aconv\<close>~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the
   basic equality relation on type \<^ML_type>\<open>term\<close>; raw datatype equality
@@ -564,41 +564,41 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Logic.all: "term -> term -> term"} \\
-  @{index_ML Logic.mk_implies: "term * term -> term"} \\
+  @{define_ML Logic.all: "term -> term -> term"} \\
+  @{define_ML Logic.mk_implies: "term * term -> term"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type ctyp} \\
-  @{index_ML_type cterm} \\
-  @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\
-  @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
-  @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
-  @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
-  @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\
-  @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
+  @{define_ML_type ctyp} \\
+  @{define_ML_type cterm} \\
+  @{define_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\
+  @{define_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
+  @{define_ML Thm.apply: "cterm -> cterm -> cterm"} \\
+  @{define_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
+  @{define_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\
+  @{define_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type thm} \\
-  @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
-  @{index_ML Thm.assume: "cterm -> thm"} \\
-  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
-  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
-  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
-  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
-  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
-  @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+  @{define_ML_type thm} \\
+  @{define_ML Thm.transfer: "theory -> thm -> thm"} \\
+  @{define_ML Thm.assume: "cterm -> thm"} \\
+  @{define_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
+  @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
+  @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
+  @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
+  @{define_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
+  @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   -> thm -> thm"} \\
-  @{index_ML Thm.add_axiom: "Proof.context ->
+  @{define_ML Thm.add_axiom: "Proof.context ->
   binding * term -> theory -> (string * thm) * theory"} \\
-  @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
+  @{define_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   (string * ('a -> thm)) * theory"} \\
-  @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->
+  @{define_ML Thm.add_def: "Defs.context -> bool -> bool ->
   binding * term -> theory -> (string * thm) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Theory.add_deps: "Defs.context -> string ->
+  @{define_ML Theory.add_deps: "Defs.context -> string ->
   Defs.entry -> Defs.entry list -> theory -> theory"} \\
-  @{index_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
+  @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
@@ -796,12 +796,12 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
-  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
-  @{index_ML Drule.mk_term: "cterm -> thm"} \\
-  @{index_ML Drule.dest_term: "thm -> cterm"} \\
-  @{index_ML Logic.mk_type: "typ -> term"} \\
-  @{index_ML Logic.dest_type: "term -> typ"} \\
+  @{define_ML Conjunction.intr: "thm -> thm -> thm"} \\
+  @{define_ML Conjunction.elim: "thm -> thm * thm"} \\
+  @{define_ML Drule.mk_term: "cterm -> thm"} \\
+  @{define_ML Drule.dest_term: "thm -> cterm"} \\
+  @{define_ML Logic.mk_type: "typ -> term"} \\
+  @{define_ML Logic.dest_type: "term -> typ"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Conjunction.intr\<close> derives \<open>A &&& B\<close> from \<open>A\<close> and \<open>B\<close>.
@@ -846,8 +846,8 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
-  @{index_ML Thm.strip_shyps: "thm -> thm"} \\
+  @{define_ML Thm.extra_shyps: "thm -> sort list"} \\
+  @{define_ML Thm.strip_shyps: "thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Thm.extra_shyps\<close>~\<open>thm\<close> determines the extraneous sort hypotheses of
@@ -951,7 +951,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
+  @{define_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Simplifier.norm_hhf\<close>~\<open>ctxt thm\<close> normalizes the given theorem
@@ -1022,14 +1022,14 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_infix "RSN": "thm * (int * thm) -> thm"} \\
-  @{index_ML_infix "RS": "thm * thm -> thm"} \\
+  @{define_ML_infix "RSN": "thm * (int * thm) -> thm"} \\
+  @{define_ML_infix "RS": "thm * thm -> thm"} \\
 
-  @{index_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\
-  @{index_ML_infix "RL": "thm list * thm list -> thm list"} \\
+  @{define_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\
+  @{define_ML_infix "RL": "thm list * thm list -> thm list"} \\
 
-  @{index_ML_infix "MRS": "thm list * thm -> thm"} \\
-  @{index_ML_infix "OF": "thm * thm list -> thm"} \\
+  @{define_ML_infix "MRS": "thm list * thm -> thm"} \\
+  @{define_ML_infix "OF": "thm * thm list -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the
@@ -1184,22 +1184,22 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type proof} \\
-  @{index_ML_type proof_body} \\
-  @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
-  @{index_ML Proofterm.reconstruct_proof:
+  @{define_ML_type proof} \\
+  @{define_ML_type proof_body} \\
+  @{define_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
+  @{define_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
-  @{index_ML Proofterm.expand_proof: "theory ->
+  @{define_ML Proofterm.expand_proof: "theory ->
   (Proofterm.thm_header -> string option) -> proof -> proof"} \\
-  @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
-  @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
-  @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
+  @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
+  @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
+  @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
-  constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_infix "%"},
-  @{index_ML_infix "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
-  Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
+  constructors @{define_ML Abst}, @{define_ML AbsP}, @{define_ML_infix "%"},
+  @{define_ML_infix "%%"}, @{define_ML PBound}, @{define_ML MinProof}, @{define_ML
+  Hyp}, @{define_ML PAxm}, @{define_ML Oracle}, @{define_ML PThm} as explained
   above. %FIXME PClass (!?)
 
   \<^descr> Type \<^ML_type>\<open>proof_body\<close> represents the nested proof information of a
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat May 22 21:52:13 2021 +0200
@@ -611,10 +611,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
-  @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
-  @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
-  @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
+  @{define_ML Context.the_generic_context: "unit -> Context.generic"} \\
+  @{define_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
+  @{define_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
+  @{define_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
     \<^descr> \<^ML>\<open>Context.the_generic_context ()\<close> refers to the theory context of
@@ -818,10 +818,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\
-  @{index_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
-  @{index_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
-  @{index_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
+  @{define_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\
+  @{define_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
+  @{define_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
+  @{define_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
   \end{mldecls}
 \<close>
 
@@ -853,9 +853,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
-  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
-  @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
+  @{define_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
+  @{define_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
+  @{define_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>fold\<close>~\<open>f\<close> lifts the parametrized update function \<open>f\<close> to a list of
@@ -969,10 +969,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML writeln: "string -> unit"} \\
-  @{index_ML tracing: "string -> unit"} \\
-  @{index_ML warning: "string -> unit"} \\
-  @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
+  @{define_ML writeln: "string -> unit"} \\
+  @{define_ML tracing: "string -> unit"} \\
+  @{define_ML warning: "string -> unit"} \\
+  @{define_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>writeln\<close>~\<open>text\<close> outputs \<open>text\<close> as regular message. This is the
@@ -1140,13 +1140,13 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
-  @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
-  @{index_ML_exception ERROR of string} \\
-  @{index_ML_exception Fail of string} \\
-  @{index_ML Exn.is_interrupt: "exn -> bool"} \\
-  @{index_ML Exn.reraise: "exn -> 'a"} \\
-  @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
+  @{define_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
+  @{define_ML can: "('a -> 'b) -> 'a -> bool"} \\
+  @{define_ML_exception ERROR of string} \\
+  @{define_ML_exception Fail of string} \\
+  @{define_ML Exn.is_interrupt: "exn -> bool"} \\
+  @{define_ML Exn.reraise: "exn -> 'a"} \\
+  @{define_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \<^rail>\<open>
@@ -1284,16 +1284,16 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Symbol.symbol = string} \\
-  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
-  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+  @{define_ML_type Symbol.symbol = string} \\
+  @{define_ML Symbol.explode: "string -> Symbol.symbol list"} \\
+  @{define_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
+  @{define_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
+  @{define_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
+  @{define_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type "Symbol.sym"} \\
-  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
+  @{define_ML_type "Symbol.sym"} \\
+  @{define_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Symbol.symbol\<close> represents individual Isabelle symbols.
@@ -1347,7 +1347,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type char} \\
+  @{define_ML_type char} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>char\<close> is \<^emph>\<open>not\<close> used. The smallest textual unit in Isabelle
@@ -1359,7 +1359,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type string} \\
+  @{define_ML_type string} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>string\<close> represents immutable vectors of 8-bit characters.
@@ -1407,7 +1407,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type int} \\
+  @{define_ML_type int} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>int\<close> represents regular mathematical integers, which are
@@ -1425,7 +1425,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Rat.rat} \\
+  @{define_ML_type Rat.rat} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Rat.rat\<close> represents rational numbers, based on the
@@ -1444,8 +1444,8 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Time.time} \\
-  @{index_ML seconds: "real -> Time.time"} \\
+  @{define_ML_type Time.time} \\
+  @{define_ML seconds: "real -> Time.time"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Time.time\<close> represents time abstractly according to the
@@ -1463,13 +1463,13 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\
-  @{index_ML is_some: "'a option -> bool"} \\
-  @{index_ML is_none: "'a option -> bool"} \\
-  @{index_ML the: "'a option -> 'a"} \\
-  @{index_ML these: "'a list option -> 'a list"} \\
-  @{index_ML the_list: "'a option -> 'a list"} \\
-  @{index_ML the_default: "'a -> 'a option -> 'a"} \\
+  @{define_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\
+  @{define_ML is_some: "'a option -> bool"} \\
+  @{define_ML is_none: "'a option -> bool"} \\
+  @{define_ML the: "'a option -> 'a"} \\
+  @{define_ML these: "'a list option -> 'a list"} \\
+  @{define_ML the_list: "'a option -> 'a list"} \\
+  @{define_ML the_default: "'a -> 'a option -> 'a"} \\
   \end{mldecls}
 \<close>
 
@@ -1490,11 +1490,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML cons: "'a -> 'a list -> 'a list"} \\
-  @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
-  @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
-  @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
-  @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
+  @{define_ML cons: "'a -> 'a list -> 'a list"} \\
+  @{define_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
+  @{define_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
+  @{define_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
+  @{define_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>cons\<close>~\<open>x xs\<close> evaluates to \<open>x :: xs\<close>.
@@ -1563,9 +1563,9 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
-  @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
-  @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
+  @{define_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
+  @{define_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
+  @{define_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>AList.lookup\<close>, \<^ML>\<open>AList.defined\<close>, \<^ML>\<open>AList.update\<close> implement the
@@ -1593,10 +1593,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "'a Unsynchronized.ref"} \\
-  @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
-  @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
-  @{index_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
+  @{define_ML_type "'a Unsynchronized.ref"} \\
+  @{define_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
+  @{define_ML "!": "'a Unsynchronized.ref -> 'a"} \\
+  @{define_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
   \end{mldecls}
 \<close>
 
@@ -1748,8 +1748,8 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML File.tmp_path: "Path.T -> Path.T"} \\
-  @{index_ML serial_string: "unit -> string"} \\
+  @{define_ML File.tmp_path: "Path.T -> Path.T"} \\
+  @{define_ML serial_string: "unit -> string"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>File.tmp_path\<close>~\<open>path\<close> relocates the base component of \<open>path\<close> into the
@@ -1790,9 +1790,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "'a Synchronized.var"} \\
-  @{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
-  @{index_ML Synchronized.guarded_access: "'a Synchronized.var ->
+  @{define_ML_type "'a Synchronized.var"} \\
+  @{define_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
+  @{define_ML Synchronized.guarded_access: "'a Synchronized.var ->
   ('a -> ('b * 'a) option) -> 'b"} \\
   \end{mldecls}
 
@@ -1890,12 +1890,12 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "'a Exn.result"} \\
-  @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
-  @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
-  @{index_ML Exn.release: "'a Exn.result -> 'a"} \\
-  @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
-  @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
+  @{define_ML_type "'a Exn.result"} \\
+  @{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{define_ML Exn.release: "'a Exn.result -> 'a"} \\
+  @{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
+  @{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a Exn.result\<close> represents the disjoint sum of ML results
@@ -1945,8 +1945,8 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\
-  @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
+  @{define_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\
+  @{define_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Par_List.map\<close>~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> is like \<^ML>\<open>map\<close>~\<open>f [x\<^sub>1, \<dots>,
@@ -2009,10 +2009,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "'a lazy"} \\
-  @{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
-  @{index_ML Lazy.value: "'a -> 'a lazy"} \\
-  @{index_ML Lazy.force: "'a lazy -> 'a"} \\
+  @{define_ML_type "'a lazy"} \\
+  @{define_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
+  @{define_ML Lazy.value: "'a -> 'a lazy"} \\
+  @{define_ML Lazy.force: "'a lazy -> 'a"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a lazy\<close> represents lazy values over type \<^verbatim>\<open>'a\<close>.
@@ -2090,17 +2090,17 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "'a future"} \\
-  @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
-  @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
-  @{index_ML Future.join: "'a future -> 'a"} \\
-  @{index_ML Future.joins: "'a future list -> 'a list"} \\
-  @{index_ML Future.value: "'a -> 'a future"} \\
-  @{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\
-  @{index_ML Future.cancel: "'a future -> unit"} \\
-  @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
-  @{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\
-  @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
+  @{define_ML_type "'a future"} \\
+  @{define_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
+  @{define_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
+  @{define_ML Future.join: "'a future -> 'a"} \\
+  @{define_ML Future.joins: "'a future list -> 'a list"} \\
+  @{define_ML Future.value: "'a -> 'a future"} \\
+  @{define_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\
+  @{define_ML Future.cancel: "'a future -> unit"} \\
+  @{define_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
+  @{define_ML Future.promise: "(unit -> unit) -> 'a future"} \\
+  @{define_ML Future.fulfill: "'a future -> 'a -> unit"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a future\<close> represents future values over type \<^verbatim>\<open>'a\<close>.
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Sat May 22 21:52:13 2021 +0200
@@ -108,12 +108,12 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type theory} \\
-  @{index_ML Context.eq_thy: "theory * theory -> bool"} \\
-  @{index_ML Context.subthy: "theory * theory -> bool"} \\
-  @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
-  @{index_ML Theory.parents_of: "theory -> theory list"} \\
-  @{index_ML Theory.ancestors_of: "theory -> theory list"} \\
+  @{define_ML_type theory} \\
+  @{define_ML Context.eq_thy: "theory * theory -> bool"} \\
+  @{define_ML Context.subthy: "theory * theory -> bool"} \\
+  @{define_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
+  @{define_ML Theory.parents_of: "theory -> theory list"} \\
+  @{define_ML Theory.ancestors_of: "theory -> theory list"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>theory\<close> represents theory contexts.
@@ -187,10 +187,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Proof.context} \\
-  @{index_ML Proof_Context.init_global: "theory -> Proof.context"} \\
-  @{index_ML Proof_Context.theory_of: "Proof.context -> theory"} \\
-  @{index_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\
+  @{define_ML_type Proof.context} \\
+  @{define_ML Proof_Context.init_global: "theory -> Proof.context"} \\
+  @{define_ML Proof_Context.theory_of: "Proof.context -> theory"} \\
+  @{define_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Proof.context\<close> represents proof contexts.
@@ -236,9 +236,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Context.generic} \\
-  @{index_ML Context.theory_of: "Context.generic -> theory"} \\
-  @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\
+  @{define_ML_type Context.generic} \\
+  @{define_ML Context.theory_of: "Context.generic -> theory"} \\
+  @{define_ML Context.proof_of: "Context.generic -> Proof.context"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Context.generic\<close> is the direct sum of \<^ML_type>\<open>theory\<close>
@@ -339,9 +339,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_functor Theory_Data} \\
-  @{index_ML_functor Proof_Data} \\
-  @{index_ML_functor Generic_Data} \\
+  @{define_ML_functor Theory_Data} \\
+  @{define_ML_functor Proof_Data} \\
+  @{define_ML_functor Generic_Data} \\
   \end{mldecls}
 
   \<^descr> \<^ML_functor>\<open>Theory_Data\<close>\<open>(spec)\<close> declares data for type \<^ML_type>\<open>theory\<close>
@@ -482,15 +482,15 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
-  @{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
-  @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
+  @{define_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
+  @{define_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
+  @{define_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
   bool Config.T"} \\
-  @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
+  @{define_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
   int Config.T"} \\
-  @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
+  @{define_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
   real Config.T"} \\
-  @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
+  @{define_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
   string Config.T"} \\
   \end{mldecls}
 
@@ -613,18 +613,18 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Name.internal: "string -> string"} \\
-  @{index_ML Name.skolem: "string -> string"} \\
+  @{define_ML Name.internal: "string -> string"} \\
+  @{define_ML Name.skolem: "string -> string"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type Name.context} \\
-  @{index_ML Name.context: Name.context} \\
-  @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
-  @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\
-  @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
+  @{define_ML_type Name.context} \\
+  @{define_ML Name.context: Name.context} \\
+  @{define_ML Name.declare: "string -> Name.context -> Name.context"} \\
+  @{define_ML Name.invent: "Name.context -> string -> int -> string list"} \\
+  @{define_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
+  @{define_ML Variable.names_of: "Proof.context -> Name.context"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Name.internal\<close>~\<open>name\<close> produces an internal name by adding one
@@ -720,7 +720,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type indexname = "string * int"} \\
+  @{define_ML_type indexname = "string * int"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>indexname\<close> represents indexed names. This is an
@@ -755,11 +755,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Long_Name.base_name: "string -> string"} \\
-  @{index_ML Long_Name.qualifier: "string -> string"} \\
-  @{index_ML Long_Name.append: "string -> string -> string"} \\
-  @{index_ML Long_Name.implode: "string list -> string"} \\
-  @{index_ML Long_Name.explode: "string -> string list"} \\
+  @{define_ML Long_Name.base_name: "string -> string"} \\
+  @{define_ML Long_Name.qualifier: "string -> string"} \\
+  @{define_ML Long_Name.append: "string -> string -> string"} \\
+  @{define_ML Long_Name.implode: "string list -> string"} \\
+  @{define_ML Long_Name.explode: "string -> string list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Long_Name.base_name\<close>~\<open>name\<close> returns the base name of a long name.
@@ -832,29 +832,29 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type binding} \\
-  @{index_ML Binding.empty: binding} \\
-  @{index_ML Binding.name: "string -> binding"} \\
-  @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
-  @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
-  @{index_ML Binding.concealed: "binding -> binding"} \\
-  @{index_ML Binding.print: "binding -> string"} \\
+  @{define_ML_type binding} \\
+  @{define_ML Binding.empty: binding} \\
+  @{define_ML Binding.name: "string -> binding"} \\
+  @{define_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
+  @{define_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
+  @{define_ML Binding.concealed: "binding -> binding"} \\
+  @{define_ML Binding.print: "binding -> string"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type Name_Space.naming} \\
-  @{index_ML Name_Space.global_naming: Name_Space.naming} \\
-  @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
-  @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
+  @{define_ML_type Name_Space.naming} \\
+  @{define_ML Name_Space.global_naming: Name_Space.naming} \\
+  @{define_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
+  @{define_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type Name_Space.T} \\
-  @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
-  @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
-  @{index_ML Name_Space.declare: "Context.generic -> bool ->
+  @{define_ML_type Name_Space.T} \\
+  @{define_ML Name_Space.empty: "string -> Name_Space.T"} \\
+  @{define_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
+  @{define_ML Name_Space.declare: "Context.generic -> bool ->
   binding -> Name_Space.T -> string * Name_Space.T"} \\
-  @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
-  @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
-  @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
+  @{define_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
+  @{define_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
+  @{define_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>binding\<close> represents the abstract concept of name bindings.
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy	Sat May 22 21:52:13 2021 +0200
@@ -92,18 +92,18 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Variable.add_fixes: "
+  @{define_ML Variable.add_fixes: "
   string list -> Proof.context -> string list * Proof.context"} \\
-  @{index_ML Variable.variant_fixes: "
+  @{define_ML Variable.variant_fixes: "
   string list -> Proof.context -> string list * Proof.context"} \\
-  @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
-  @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
-  @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
-  @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
-  @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
+  @{define_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
+  @{define_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
+  @{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
+  @{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
+  @{define_ML Variable.import: "bool -> thm list -> Proof.context ->
   ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
     * Proof.context"} \\
-  @{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
+  @{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
   ((string * (string * typ)) list * term) * Proof.context"} \\
   \end{mldecls}
 
@@ -263,14 +263,14 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type Assumption.export} \\
-  @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
-  @{index_ML Assumption.add_assms:
+  @{define_ML_type Assumption.export} \\
+  @{define_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
+  @{define_ML Assumption.add_assms:
     "Assumption.export ->
   cterm list -> Proof.context -> thm list * Proof.context"} \\
-  @{index_ML Assumption.add_assumes: "
+  @{define_ML Assumption.add_assumes: "
   cterm list -> Proof.context -> thm list * Proof.context"} \\
-  @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+  @{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents arbitrary export rules, which
@@ -359,31 +359,31 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
+  @{define_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
-  @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
+  @{define_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
-  @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
+  @{define_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
-  @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
+  @{define_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
-  @{index_ML Subgoal.focus: "Proof.context -> int -> binding list option ->
+  @{define_ML Subgoal.focus: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
-  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option ->
+  @{define_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
-  @{index_ML Subgoal.focus_params: "Proof.context -> int -> binding list option ->
+  @{define_ML Subgoal.focus_params: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
   \end{mldecls}
 
   \begin{mldecls}
-  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
+  @{define_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
-  @{index_ML Goal.prove_common: "Proof.context -> int option ->
+  @{define_ML Goal.prove_common: "Proof.context -> int option ->
   string list -> term list -> term list ->
   ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
+  @{define_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
   Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   \end{mldecls}
 
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Syntax.thy	Sat May 22 21:52:13 2021 +0200
@@ -69,16 +69,16 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\
-  @{index_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\
-  @{index_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex]
-  @{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
-  @{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\
-  @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex]
-  @{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
-  @{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
-  @{index_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\
-  @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
+  @{define_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\
+  @{define_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\
+  @{define_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex]
+  @{define_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
+  @{define_ML Syntax.read_term: "Proof.context -> string -> term"} \\
+  @{define_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex]
+  @{define_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{define_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
+  @{define_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\
+  @{define_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.read_typs\<close>~\<open>ctxt strs\<close> parses and checks a simultaneous list
@@ -158,11 +158,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
-  @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
-  @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
-  @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
-  @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
+  @{define_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
+  @{define_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
+  @{define_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
+  @{define_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{define_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.parse_typ\<close>~\<open>ctxt str\<close> parses a source string as pre-type that
@@ -219,11 +219,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
-  @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
-  @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
-  @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
-  @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
+  @{define_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
+  @{define_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
+  @{define_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
+  @{define_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
+  @{define_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.check_typs\<close>~\<open>ctxt Ts\<close> checks a simultaneous list of pre-types
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Sat May 22 21:52:13 2021 +0200
@@ -61,10 +61,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Goal.init: "cterm -> thm"} \\
-  @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
-  @{index_ML Goal.protect: "int -> thm -> thm"} \\
-  @{index_ML Goal.conclude: "thm -> thm"} \\
+  @{define_ML Goal.init: "cterm -> thm"} \\
+  @{define_ML Goal.finish: "Proof.context -> thm -> thm"} \\
+  @{define_ML Goal.protect: "int -> thm -> thm"} \\
+  @{define_ML Goal.conclude: "thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Goal.init\<close>~\<open>C\<close> initializes a tactical goal from the well-formed
@@ -156,15 +156,15 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type tactic = "thm -> thm Seq.seq"} \\
-  @{index_ML no_tac: tactic} \\
-  @{index_ML all_tac: tactic} \\
-  @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
-  @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
-  @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
-  @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
-  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
-  @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
+  @{define_ML_type tactic = "thm -> thm Seq.seq"} \\
+  @{define_ML no_tac: tactic} \\
+  @{define_ML all_tac: tactic} \\
+  @{define_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
+  @{define_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
+  @{define_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
+  @{define_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
+  @{define_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
+  @{define_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>tactic\<close> represents tactics. The well-formedness conditions
@@ -243,17 +243,17 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex]
-  @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\
-  @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
-  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
+  @{define_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex]
+  @{define_ML assume_tac: "Proof.context -> int -> tactic"} \\
+  @{define_ML eq_assume_tac: "int -> tactic"} \\[1ex]
+  @{define_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>resolve_tac\<close>~\<open>ctxt thms i\<close> refines the goal state using the given
@@ -351,23 +351,23 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Rule_Insts.res_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.res_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.eres_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.eres_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.dres_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.dres_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.forw_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.forw_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
+  @{define_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
     (binding * string option * mixfix) list -> int -> tactic"} \\
-  @{index_ML Rule_Insts.thin_tac: "Proof.context -> string ->
+  @{define_ML Rule_Insts.thin_tac: "Proof.context -> string ->
     (binding * string option * mixfix) list -> int -> tactic"} \\
-  @{index_ML rename_tac: "string list -> int -> tactic"} \\
+  @{define_ML rename_tac: "string list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Rule_Insts.res_inst_tac\<close>~\<open>ctxt insts thm i\<close> instantiates the rule
@@ -415,9 +415,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML rotate_tac: "int -> int -> tactic"} \\
-  @{index_ML distinct_subgoals_tac: tactic} \\
-  @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
+  @{define_ML rotate_tac: "int -> int -> tactic"} \\
+  @{define_ML distinct_subgoals_tac: tactic} \\
+  @{define_ML flexflex_tac: "Proof.context -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>rotate_tac\<close>~\<open>n i\<close> rotates the premises of subgoal \<open>i\<close> by \<open>n\<close>
@@ -450,9 +450,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
-  @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
-  @{index_ML_infix COMP: "thm * thm -> thm"} \\
+  @{define_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
+  @{define_ML Drule.compose: "thm * int * thm -> thm"} \\
+  @{define_ML_infix COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>compose_tac\<close>~\<open>ctxt (flag, rule, m) i\<close> refines subgoal \<open>i\<close> using
@@ -502,17 +502,17 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_infix "THEN": "tactic * tactic -> tactic"} \\
-  @{index_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
-  @{index_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
-  @{index_ML "EVERY": "tactic list -> tactic"} \\
-  @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
+  @{define_ML_infix "THEN": "tactic * tactic -> tactic"} \\
+  @{define_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
+  @{define_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
+  @{define_ML "EVERY": "tactic list -> tactic"} \\
+  @{define_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
 
-  @{index_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
-  @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
+  @{define_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
+  @{define_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>2\<close> is the sequential composition of \<open>tac\<^sub>1\<close> and
@@ -555,11 +555,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML "TRY": "tactic -> tactic"} \\
-  @{index_ML "REPEAT": "tactic -> tactic"} \\
-  @{index_ML "REPEAT1": "tactic -> tactic"} \\
-  @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
-  @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
+  @{define_ML "TRY": "tactic -> tactic"} \\
+  @{define_ML "REPEAT": "tactic -> tactic"} \\
+  @{define_ML "REPEAT1": "tactic -> tactic"} \\
+  @{define_ML "REPEAT_DETERM": "tactic -> tactic"} \\
+  @{define_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>TRY\<close>~\<open>tac\<close> applies \<open>tac\<close> to the goal state and returns the resulting
@@ -641,13 +641,13 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
-  @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
-  @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
-  @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
+  @{define_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
+  @{define_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
+  @{define_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
+  @{define_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>ALLGOALS\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_op>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac 1\<close>. It applies the \<open>tac\<close> to all the subgoals, counting downwards.
@@ -689,8 +689,8 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML CHANGED: "tactic -> tactic"} \\
+  @{define_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML CHANGED: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>FILTER\<close>~\<open>sat tac\<close> applies \<open>tac\<close> to the goal state and returns a
@@ -706,9 +706,9 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\
-  @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
+  @{define_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML DEPTH_SOLVE: "tactic -> tactic"} \\
+  @{define_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>DEPTH_FIRST\<close>~\<open>sat tac\<close> returns the goal state if \<open>sat\<close> returns true.
@@ -729,9 +729,9 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
-  @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  @{define_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  @{define_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
   \end{mldecls}
 
   These search strategies will find a solution if one exists. However, they do
@@ -763,10 +763,10 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
-  @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\
-  @{index_ML SOLVE: "tactic -> tactic"} \\
-  @{index_ML DETERM: "tactic -> tactic"} \\
+  @{define_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
+  @{define_ML IF_UNSOLVED: "tactic -> tactic"} \\
+  @{define_ML SOLVE: "tactic -> tactic"} \\
+  @{define_ML DETERM: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>COND\<close>~\<open>sat tac\<^sub>1 tac\<^sub>2\<close> applies \<open>tac\<^sub>1\<close> to the goal state if it
@@ -792,10 +792,10 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML has_fewer_prems: "int -> thm -> bool"} \\
-  @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\
-  @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
-  @{index_ML size_of_thm: "thm -> int"} \\
+  @{define_ML has_fewer_prems: "int -> thm -> bool"} \\
+  @{define_ML Thm.eq_thm: "thm * thm -> bool"} \\
+  @{define_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
+  @{define_ML size_of_thm: "thm -> int"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>has_fewer_prems\<close>~\<open>n thm\<close> reports whether \<open>thm\<close> has fewer than \<open>n\<close>
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Sat May 22 21:52:13 2021 +0200
@@ -638,7 +638,7 @@
   of the term ordering.
 
   The default is lexicographic ordering of term structure, but this could be
-  also changed locally for special applications via @{index_ML
+  also changed locally for special applications via @{define_ML
   Simplifier.set_term_ord} in Isabelle/ML.
 
   \<^medskip>
@@ -866,9 +866,9 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) ->
+  @{define_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) ->
   Proof.context -> Proof.context"} \\
-  @{index_ML Simplifier.prems_of: "Proof.context -> thm list"} \\
+  @{define_ML Simplifier.prems_of: "Proof.context -> thm list"} \\
   \end{mldecls}
 
   The subgoaler is the tactic used to solve subgoals arising out of
@@ -906,13 +906,13 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML_type solver} \\
-  @{index_ML Simplifier.mk_solver: "string ->
+  @{define_ML_type solver} \\
+  @{define_ML Simplifier.mk_solver: "string ->
   (Proof.context -> int -> tactic) -> solver"} \\
-  @{index_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
   \end{mldecls}
 
   A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -992,17 +992,17 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML_infix setloop: "Proof.context *
+  @{define_ML_infix setloop: "Proof.context *
   (Proof.context -> int -> tactic) -> Proof.context"} \\
-  @{index_ML_infix addloop: "Proof.context *
+  @{define_ML_infix addloop: "Proof.context *
   (string * (Proof.context -> int -> tactic))
   -> Proof.context"} \\
-  @{index_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
-  @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
-  @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
-  @{index_ML Splitter.add_split_bang: "
+  @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
+  @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
+  @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
+  @{define_ML Splitter.add_split_bang: "
   thm -> Proof.context -> Proof.context"} \\
-  @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
+  @{define_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   The looper is a list of tactics that are applied after simplification, in
@@ -1624,23 +1624,23 @@
 
 text \<open>
   \begin{mldecls}
-    @{index_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
-    @{index_ML_infix addSWrapper: "Proof.context *
+    @{define_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
+    @{define_ML_infix addSWrapper: "Proof.context *
   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
-    @{index_ML_infix addSbefore: "Proof.context *
+    @{define_ML_infix addSbefore: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_infix addSafter: "Proof.context *
+    @{define_ML_infix addSafter: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
-    @{index_ML_infix addWrapper: "Proof.context *
+    @{define_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+    @{define_ML_infix addWrapper: "Proof.context *
   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
-    @{index_ML_infix addbefore: "Proof.context *
+    @{define_ML_infix addbefore: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_infix addafter: "Proof.context *
+    @{define_ML_infix addafter: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
-    @{index_ML addSss: "Proof.context -> Proof.context"} \\
-    @{index_ML addss: "Proof.context -> Proof.context"} \\
+    @{define_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+    @{define_ML addSss: "Proof.context -> Proof.context"} \\
+    @{define_ML addss: "Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   The proof strategy of the Classical Reasoner is simple.  Perform as
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat May 22 21:52:13 2021 +0200
@@ -220,8 +220,8 @@
 
 text \<open>
   \begin{mldecls}
-    @{index_ML print_mode_value: "unit -> string list"} \\
-    @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
+    @{define_ML print_mode_value: "unit -> string list"} \\
+    @{define_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   \end{mldecls}
 
   The \<^emph>\<open>print mode\<close> facility allows to modify various operations for printing.
diff -r eccc4a13216d -r 35d8132633c6 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/antiquote_setup.ML	Sat May 22 21:52:13 2021 +0200
@@ -111,12 +111,12 @@
 
 val _ =
   Theory.setup
-   (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>index_ML\<close> #>
-    antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>index_ML_infix\<close> #>
-    antiquotation_ml' parse_type test_type "type" \<^binding>\<open>index_ML_type\<close> #>
-    antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>index_ML_exception\<close> #>
-    antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>index_ML_structure\<close> #>
-    antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>index_ML_functor\<close>);
+   (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>define_ML\<close> #>
+    antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>define_ML_infix\<close> #>
+    antiquotation_ml' parse_type test_type "type" \<^binding>\<open>define_ML_type\<close> #>
+    antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>define_ML_exception\<close> #>
+    antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>define_ML_structure\<close> #>
+    antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>define_ML_functor\<close>);
 
 end;