--- a/src/Doc/Implementation/Proof.thy Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy Thu Sep 09 12:33:14 2021 +0200
@@ -101,7 +101,7 @@
@{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 ->
- ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
+ ((ctyp TVars.table * cterm Vars.table) * thm list)
* Proof.context"} \\
@{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
((string * (string * typ)) list * term) * Proof.context"} \\