diff --git a/src/Doc/Implementation/Proof.thy b/src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy
+++ b/src/Doc/Implementation/Proof.thy
@@ -1,473 +1,473 @@
 (*:maxLineLen=78:*)
 
 theory Proof
 imports Base
 begin
 
 chapter \<open>Structured proofs\<close>
 
 section \<open>Variables \label{sec:variables}\<close>
 
 text \<open>
   Any variable that is not explicitly bound by \<open>\<lambda>\<close>-abstraction is considered
   as ``free''. Logically, free variables act like outermost universal
   quantification at the sequent level: \<open>A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)\<close> means that
   the result holds \<^emph>\<open>for all\<close> values of \<open>x\<close>. Free variables for terms (not
   types) can be fully internalized into the logic: \<open>\<turnstile> B(x)\<close> and \<open>\<turnstile> \<And>x. B(x)\<close>
   are interchangeable, provided that \<open>x\<close> does not occur elsewhere in the
   context. Inspecting \<open>\<turnstile> \<And>x. B(x)\<close> more closely, we see that inside the
   quantifier, \<open>x\<close> is essentially ``arbitrary, but fixed'', while from outside
   it appears as a place-holder for instantiation (thanks to \<open>\<And>\<close> elimination).
 
   The Pure logic represents the idea of variables being either inside or
   outside the current scope by providing separate syntactic categories for
   \<^emph>\<open>fixed variables\<close> (e.g.\ \<open>x\<close>) vs.\ \<^emph>\<open>schematic variables\<close> (e.g.\ \<open>?x\<close>).
   Incidently, a universal result \<open>\<turnstile> \<And>x. B(x)\<close> has the HHF normal form \<open>\<turnstile>
   B(?x)\<close>, which represents its generality without requiring an explicit
   quantifier. The same principle works for type variables: \<open>\<turnstile> B(?\<alpha>)\<close>
   represents the idea of ``\<open>\<turnstile> \<forall>\<alpha>. B(\<alpha>)\<close>'' without demanding a truly
   polymorphic framework.
 
   \<^medskip>
   Additional care is required to treat type variables in a way that
   facilitates type-inference. In principle, term variables depend on type
   variables, which means that type variables would have to be declared first.
   For example, a raw type-theoretic framework would demand the context to be
   constructed in stages as follows: \<open>\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)\<close>.
 
   We allow a slightly less formalistic mode of operation: term variables \<open>x\<close>
   are fixed without specifying a type yet (essentially \<^emph>\<open>all\<close> potential
   occurrences of some instance \<open>x\<^sub>\<tau>\<close> are fixed); the first occurrence of \<open>x\<close>
   within a specific term assigns its most general type, which is then
   maintained consistently in the context. The above example becomes \<open>\<Gamma> = x:
   term, \<alpha>: type, A(x\<^sub>\<alpha>)\<close>, where type \<open>\<alpha>\<close> is fixed \<^emph>\<open>after\<close> term \<open>x\<close>, and the
   constraint \<open>x :: \<alpha>\<close> is an implicit consequence of the occurrence of \<open>x\<^sub>\<alpha>\<close> in
   the subsequent proposition.
 
   This twist of dependencies is also accommodated by the reverse operation of
   exporting results from a context: a type variable \<open>\<alpha>\<close> is considered fixed as
   long as it occurs in some fixed term variable of the context. For example,
   exporting \<open>x: term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> produces in the first step \<open>x: term
   \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> for fixed \<open>\<alpha>\<close>, and only in the second step \<open>\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>\<close>
   for schematic \<open>?x\<close> and \<open>?\<alpha>\<close>. The following Isar source text illustrates this
   scenario.
 \<close>
 
 notepad
 begin
   {
     fix x  \<comment> \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
     {
       have "x::'a \<equiv> x"  \<comment> \<open>implicit type assignment by concrete occurrence\<close>
         by (rule reflexive)
     }
     thm this  \<comment> \<open>result still with fixed type \<open>'a\<close>\<close>
   }
   thm this  \<comment> \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
 end
 
 text \<open>
   The Isabelle/Isar proof context manages the details of term vs.\ type
   variables, with high-level principles for moving the frontier between fixed
   and schematic variables.
 
   The \<open>add_fixes\<close> operation explicitly declares fixed variables; the
   \<open>declare_term\<close> operation absorbs a term into a context by fixing new type
   variables and adding syntactic constraints.
 
   The \<open>export\<close> operation is able to perform the main work of generalizing term
   and type variables as sketched above, assuming that fixing variables and
   terms have been declared properly.
 
   There \<open>import\<close> operation makes a generalized fact a genuine part of the
   context, by inventing fixed variables for the schematic ones. The effect can
   be reversed by using \<open>export\<close> later, potentially with an extended context;
   the result is equivalent to the original modulo renaming of schematic
   variables.
 
   The \<open>focus\<close> operation provides a variant of \<open>import\<close> for nested propositions
   (with explicit quantification): \<open>\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)\<close> is decomposed
   by inventing fixed variables \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> for the body.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML Variable.add_fixes: "
   string list -> Proof.context -> string list * Proof.context"} \\
   @{define_ML Variable.variant_fixes: "
   string list -> Proof.context -> string 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)
+  ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
     * Proof.context"} \\
   @{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
   ((string * (string * typ)) list * term) * Proof.context"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Variable.add_fixes\<close>~\<open>xs ctxt\<close> fixes term variables \<open>xs\<close>, returning
   the resulting internal names. By default, the internal representation
   coincides with the external one, which also means that the given variables
   must not be fixed already. There is a different policy within a local proof
   body: the given names are just hints for newly invented Skolem variables.
 
   \<^descr> \<^ML>\<open>Variable.variant_fixes\<close> is similar to \<^ML>\<open>Variable.add_fixes\<close>, but
   always produces fresh variants of the given names.
 
   \<^descr> \<^ML>\<open>Variable.declare_term\<close>~\<open>t ctxt\<close> declares term \<open>t\<close> to belong to the
   context. This automatically fixes new type variables, but not term
   variables. Syntactic constraints for type and term variables are declared
   uniformly, though.
 
   \<^descr> \<^ML>\<open>Variable.declare_constraints\<close>~\<open>t ctxt\<close> declares syntactic constraints
   from term \<open>t\<close>, without making it part of the context yet.
 
   \<^descr> \<^ML>\<open>Variable.export\<close>~\<open>inner outer thms\<close> generalizes fixed type and term
   variables in \<open>thms\<close> according to the difference of the \<open>inner\<close> and \<open>outer\<close>
   context, following the principles sketched above.
 
   \<^descr> \<^ML>\<open>Variable.polymorphic\<close>~\<open>ctxt ts\<close> generalizes type variables in \<open>ts\<close> as
   far as possible, even those occurring in fixed term variables. The default
   policy of type-inference is to fix newly introduced type variables, which is
   essentially reversed with \<^ML>\<open>Variable.polymorphic\<close>: here the given terms
   are detached from the context as far as possible.
 
   \<^descr> \<^ML>\<open>Variable.import\<close>~\<open>open thms ctxt\<close> invents fixed type and term
   variables for the schematic ones occurring in \<open>thms\<close>. The \<open>open\<close> flag
   indicates whether the fixed names should be accessible to the user,
   otherwise newly introduced names are marked as ``internal''
   (\secref{sec:names}).
 
   \<^descr> \<^ML>\<open>Variable.focus\<close>~\<open>bindings B\<close> decomposes the outermost \<open>\<And>\<close> prefix of
   proposition \<open>B\<close>, using the given name bindings.
 \<close>
 
 text %mlex \<open>
   The following example shows how to work with fixed term and type parameters
   and with type-inference.
 \<close>
 
 ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = \<^context>;
 
   (*locally fixed parameters -- no type assignment yet*)
   val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"];
 
   (*t1: most general fixed type; t1': most general arbitrary type*)
   val t1 = Syntax.read_term ctxt1 "x";
   val t1' = singleton (Variable.polymorphic ctxt1) t1;
 
   (*term u enforces specific type assignment*)
   val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y";
 
   (*official declaration of u -- propagates constraints etc.*)
   val ctxt2 = ctxt1 |> Variable.declare_term u;
   val t2 = Syntax.read_term ctxt2 "x";  (*x::nat is enforced*)
 \<close>
 
 text \<open>
   In the above example, the starting context is derived from the toplevel
   theory, which means that fixed variables are internalized literally: \<open>x\<close> is
   mapped again to \<open>x\<close>, and attempting to fix it again in the subsequent
   context is an error. Alternatively, fixed parameters can be renamed
   explicitly as follows:
 \<close>
 
 ML_val \<open>
   val ctxt0 = \<^context>;
   val ([x1, x2, x3], ctxt1) =
     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
 \<close>
 
 text \<open>
   The following ML code can now work with the invented names of \<open>x1\<close>, \<open>x2\<close>,
   \<open>x3\<close>, without depending on the details on the system policy for introducing
   these variants. Recall that within a proof body the system always invents
   fresh ``Skolem constants'', e.g.\ as follows:
 \<close>
 
 notepad
 begin
   ML_prf %"ML"
    \<open>val ctxt0 = \<^context>;
 
     val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"];
     val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"];
     val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"];
 
     val ([y1, y2], ctxt4) =
       ctxt3 |> Variable.variant_fixes ["y", "y"];\<close>
 end
 
 text \<open>
   In this situation \<^ML>\<open>Variable.add_fixes\<close> and \<^ML>\<open>Variable.variant_fixes\<close>
   are very similar, but identical name proposals given in a row are only
   accepted by the second version.
 \<close>
 
 
 section \<open>Assumptions \label{sec:assumptions}\<close>
 
 text \<open>
   An \<^emph>\<open>assumption\<close> is a proposition that it is postulated in the current
   context. Local conclusions may use assumptions as additional facts, but this
   imposes implicit hypotheses that weaken the overall statement.
 
   Assumptions are restricted to fixed non-schematic statements, i.e.\ all
   generality needs to be expressed by explicit quantifiers. Nevertheless, the
   result will be in HHF normal form with outermost quantifiers stripped. For
   example, by assuming \<open>\<And>x :: \<alpha>. P x\<close> we get \<open>\<And>x :: \<alpha>. P x \<turnstile> P ?x\<close> for
   schematic \<open>?x\<close> of fixed type \<open>\<alpha>\<close>. Local derivations accumulate more and more
   explicit references to hypotheses: \<open>A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B\<close> where \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close>
   needs to be covered by the assumptions of the current context.
 
   \<^medskip>
   The \<open>add_assms\<close> operation augments the context by local assumptions, which
   are parameterized by an arbitrary \<open>export\<close> rule (see below).
 
   The \<open>export\<close> operation moves facts from a (larger) inner context into a
   (smaller) outer context, by discharging the difference of the assumptions as
   specified by the associated export rules. Note that the discharged portion
   is determined by the difference of contexts, not the facts being exported!
   There is a separate flag to indicate a goal context, where the result is
   meant to refine an enclosing sub-goal of a structured proof state.
 
   \<^medskip>
   The most basic export rule discharges assumptions directly by means of the
   \<open>\<Longrightarrow>\<close> introduction rule:
   \[
   \infer[(\<open>\<Longrightarrow>\<hyphen>intro\<close>)]{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
   \]
 
   The variant for goal refinements marks the newly introduced premises, which
   causes the canonical Isar goal refinement scheme to enforce unification with
   local premises within the goal:
   \[
   \infer[(\<open>#\<Longrightarrow>\<hyphen>intro\<close>)]{\<open>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
   \]
 
   \<^medskip>
   Alternative versions of assumptions may perform arbitrary transformations on
   export, as long as the corresponding portion of hypotheses is removed from
   the given facts. For example, a local definition works by fixing \<open>x\<close> and
   assuming \<open>x \<equiv> t\<close>, with the following export rule to reverse the effect:
   \[
   \infer[(\<open>\<equiv>\<hyphen>expand\<close>)]{\<open>\<Gamma> - (x \<equiv> t) \<turnstile> B t\<close>}{\<open>\<Gamma> \<turnstile> B x\<close>}
   \]
   This works, because the assumption \<open>x \<equiv> t\<close> was introduced in a context with
   \<open>x\<close> being fresh, so \<open>x\<close> does not occur in \<open>\<Gamma>\<close> here.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{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"} \\
   @{define_ML Assumption.add_assumes: "
   cterm list -> Proof.context -> thm list * Proof.context"} \\
   @{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
   is any function of type \<^ML_type>\<open>bool -> cterm list -> thm -> thm\<close>, where
   the \<^ML_type>\<open>bool\<close> indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
   the collection of assumptions to be discharged simultaneously.
 
   \<^descr> \<^ML>\<open>Assumption.assume\<close>~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive
   assumption \<open>A \<turnstile> A'\<close>, where the conclusion \<open>A'\<close> is in HHF normal form.
 
   \<^descr> \<^ML>\<open>Assumption.add_assms\<close>~\<open>r As\<close> augments the context by assumptions \<open>As\<close>
   with export rule \<open>r\<close>. The resulting facts are hypothetical theorems as
   produced by the raw \<^ML>\<open>Assumption.assume\<close>.
 
   \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
   \<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
 
   \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
   from the the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close>
   means this is a goal context. The result is in HHF normal form. Note that
   \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and \<^ML>\<open>Assumption.export\<close> in the canonical way.
 \<close>
 
 text %mlex \<open>
   The following example demonstrates how rules can be derived by building up a
   context of assumptions first, and exporting some local fact afterwards. We
   refer to \<^theory>\<open>Pure\<close> equality here for testing purposes.
 \<close>
 
 ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = \<^context>;
 
   val ([eq], ctxt1) =
     ctxt0 |> Assumption.add_assumes [\<^cprop>\<open>x \<equiv> y\<close>];
   val eq' = Thm.symmetric eq;
 
   (*back to original context -- discharges assumption*)
   val r = Assumption.export false ctxt1 ctxt0 eq';
 \<close>
 
 text \<open>
   Note that the variables of the resulting rule are not generalized. This
   would have required to fix them properly in the context beforehand, and
   export wrt.\ variables afterwards (cf.\ \<^ML>\<open>Variable.export\<close> or the
   combined \<^ML>\<open>Proof_Context.export\<close>).
 \<close>
 
 
 section \<open>Structured goals and results \label{sec:struct-goals}\<close>
 
 text \<open>
   Local results are established by monotonic reasoning from facts within a
   context. This allows common combinations of theorems, e.g.\ via \<open>\<And>/\<Longrightarrow>\<close>
   elimination, resolution rules, or equational reasoning, see
   \secref{sec:thms}. Unaccounted context manipulations should be avoided,
   notably raw \<open>\<And>/\<Longrightarrow>\<close> introduction or ad-hoc references to free variables or
   assumptions not present in the proof context.
 
   \<^medskip>
   The \<open>SUBPROOF\<close> combinator allows to structure a tactical proof recursively
   by decomposing a selected sub-goal: \<open>(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>\<close> is turned into
   \<open>B(x) \<Longrightarrow> \<dots>\<close> after fixing \<open>x\<close> and assuming \<open>A(x)\<close>. This means the tactic needs
   to solve the conclusion, but may use the premise as a local fact, for
   locally fixed variables.
 
   The family of \<open>FOCUS\<close> combinators is similar to \<open>SUBPROOF\<close>, but allows to
   retain schematic variables and pending subgoals in the resulting goal state.
 
   The \<open>prove\<close> operation provides an interface for structured backwards
   reasoning under program control, with some explicit sanity checks of the
   result. The goal context can be augmented by additional fixed variables
   (cf.\ \secref{sec:variables}) and assumptions (cf.\
   \secref{sec:assumptions}), which will be available as local facts during the
   proof and discharged into implications in the result. Type and term
   variables are generalized as usual, according to the context.
 
   The \<open>obtain\<close> operation produces results by eliminating existing facts by
   means of a given tactic. This acts like a dual conclusion: the proof
   demonstrates that the context may be augmented by parameters and
   assumptions, without affecting any conclusions that do not mention these
   parameters. See also @{cite "isabelle-isar-ref"} for the user-level
   @{command obtain} and @{command guess} elements. Final results, which may
   not refer to the parameters in the conclusion, need to exported explicitly
   into the original context.\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
   @{define_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
   @{define_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
   @{define_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
   @{define_ML Subgoal.focus: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
   @{define_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
   @{define_ML Subgoal.focus_params: "Proof.context -> int -> binding list option ->
   thm -> Subgoal.focus * thm"} \\
   \end{mldecls}
 
   \begin{mldecls}
   @{define_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
   @{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}
   @{define_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
   Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>SUBPROOF\<close>~\<open>tac ctxt i\<close> decomposes the structure of the specified
   sub-goal, producing an extended context and a reduced goal, which needs to
   be solved by the given tactic. All schematic parameters of the goal are
   imported into the context as fixed ones, which may not be instantiated in
   the sub-proof.
 
   \<^descr> \<^ML>\<open>Subgoal.FOCUS\<close>, \<^ML>\<open>Subgoal.FOCUS_PREMS\<close>, and \<^ML>\<open>Subgoal.FOCUS_PARAMS\<close> are similar to \<^ML>\<open>SUBPROOF\<close>, but are slightly more
   flexible: only the specified parts of the subgoal are imported into the
   context, and the body tactic may introduce new subgoals and schematic
   variables.
 
   \<^descr> \<^ML>\<open>Subgoal.focus\<close>, \<^ML>\<open>Subgoal.focus_prems\<close>, \<^ML>\<open>Subgoal.focus_params\<close>
   extract the focus information from a goal state in the same way as the
   corresponding tacticals above. This is occasionally useful to experiment
   without writing actual tactics yet.
 
   \<^descr> \<^ML>\<open>Goal.prove\<close>~\<open>ctxt xs As C tac\<close> states goal \<open>C\<close> in the context
   augmented by fixed variables \<open>xs\<close> and assumptions \<open>As\<close>, and applies tactic
   \<open>tac\<close> to solve it. The latter may depend on the local assumptions being
   presented as facts. The result is in HHF normal form.
 
   \<^descr> \<^ML>\<open>Goal.prove_common\<close>~\<open>ctxt fork_pri\<close> is the common form to state and
   prove a simultaneous goal statement, where \<^ML>\<open>Goal.prove\<close> is a convenient
   shorthand that is most frequently used in applications.
 
   The given list of simultaneous conclusions is encoded in the goal state by
   means of Pure conjunction: \<^ML>\<open>Goal.conjunction_tac\<close> will turn this into a
   collection of individual subgoals, but note that the original multi-goal
   state is usually required for advanced induction.
 
   It is possible to provide an optional priority for a forked proof, typically
   \<^ML>\<open>SOME ~1\<close>, while \<^ML>\<open>NONE\<close> means the proof is immediate (sequential)
   as for \<^ML>\<open>Goal.prove\<close>. Note that a forked proof does not exhibit any
   failures in the usual way via exceptions in ML, but accumulates error
   situations under the execution id of the running transaction. Thus the
   system is able to expose error messages ultimately to the end-user, even
   though the subsequent ML code misses them.
 
   \<^descr> \<^ML>\<open>Obtain.result\<close>~\<open>tac thms ctxt\<close> eliminates the given facts using a
   tactic, which results in additional fixed variables and assumptions in the
   context. Final results need to be exported explicitly.
 \<close>
 
 text %mlex \<open>
   The following minimal example illustrates how to access the focus
   information of a structured goal state.
 \<close>
 
 notepad
 begin
   fix A B C :: "'a \<Rightarrow> bool"
 
   have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
     ML_val
      \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};
       val (focus as {params, asms, concl, ...}, goal') =
         Subgoal.focus goal_ctxt 1 (SOME [\<^binding>\<open>x\<close>]) goal;
       val [A, B] = #prems focus;
       val [(_, x)] = #params focus;\<close>
     sorry
 end
 
 text \<open>
   \<^medskip>
   The next example demonstrates forward-elimination in a local context, using
   \<^ML>\<open>Obtain.result\<close>.
 \<close>
 
 notepad
 begin
   assume ex: "\<exists>x. B x"
 
   ML_prf %"ML"
    \<open>val ctxt0 = \<^context>;
     val (([(_, x)], [B]), ctxt1) = ctxt0
       |> Obtain.result (fn _ => eresolve_tac ctxt0 @{thms exE} 1) [@{thm ex}];\<close>
   ML_prf %"ML"
    \<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>
   ML_prf %"ML"
    \<open>Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
       handle ERROR msg => (warning msg; []);\<close>
 end
 
 end
diff --git a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
@@ -1,1227 +1,1227 @@
 (*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     Author:     Lukas Bulwahn, TU Muenchen
 
 Auxilary functions for predicate compiler.
 *)
 
 signature PREDICATE_COMPILE_AUX =
 sig
   val find_indices : ('a -> bool) -> 'a list -> int list
   (* mode *)
   datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
   val eq_mode : mode * mode -> bool
   val mode_ord: mode ord
   val list_fun_mode : mode list -> mode
   val strip_fun_mode : mode -> mode list
   val dest_fun_mode : mode -> mode list
   val dest_tuple_mode : mode -> mode list
   val all_modes_of_typ : typ -> mode list
   val all_smodes_of_typ : typ -> mode list
   val fold_map_aterms_prodT : ('a -> 'a -> 'a) -> (typ -> 'b -> 'a * 'b) -> typ -> 'b -> 'a * 'b
   val map_filter_prod : (term -> term option) -> term -> term option
   val replace_ho_args : mode -> term list -> term list -> term list
   val ho_arg_modes_of : mode -> mode list
   val ho_argsT_of : mode -> typ list -> typ list
   val ho_args_of : mode -> term list -> term list
   val ho_args_of_typ : typ -> term list -> term list
   val ho_argsT_of_typ : typ list -> typ list
   val split_map_mode : (mode -> term -> term option * term option)
     -> mode -> term list -> term list * term list
   val split_map_modeT : (mode -> typ -> typ option * typ option)
     -> mode -> typ list -> typ list * typ list
   val split_mode : mode -> term list -> term list * term list
   val split_modeT : mode -> typ list -> typ list * typ list
   val string_of_mode : mode -> string
   val ascii_string_of_mode : mode -> string
   (* premises *)
   datatype indprem = Prem of term | Negprem of term | Sidecond of term
     | Generator of (string * typ)
   val dest_indprem : indprem -> term
   val map_indprem : (term -> term) -> indprem -> indprem
   (* general syntactic functions *)
   val is_equationlike : thm -> bool
   val is_pred_equation : thm -> bool
   val is_intro : string -> thm -> bool
   val is_predT : typ -> bool
   val lookup_constr : Proof.context -> (string * typ) -> int option
   val is_constrt : Proof.context -> term -> bool
   val strip_ex : term -> (string * typ) list * term
   val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
   val strip_all : term -> (string * typ) list * term
   val strip_intro_concl : thm -> term * term list
   (* introduction rule combinators *)
   val map_atoms : (term -> term) -> term -> term
   val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_map_atoms : (term -> 'a -> term * 'a) -> term -> 'a -> term * 'a
   val maps_premises : (term -> term list) -> term -> term
   val map_concl : (term -> term) -> term -> term
   val map_term : theory -> (term -> term) -> thm -> thm
   (* split theorems of case expressions *)
   val prepare_split_thm : Proof.context -> thm -> thm
   val find_split_thm : theory -> term -> thm option
   (* datastructures and setup for generic compilation *)
   datatype compilation_funs = CompilationFuns of {
     mk_monadT : typ -> typ,
     dest_monadT : typ -> typ,
     mk_empty : typ -> term,
     mk_single : term -> term,
     mk_bind : term * term -> term,
     mk_plus : term * term -> term,
     mk_if : term -> term,
     mk_iterate_upto : typ -> term * term * term -> term,
     mk_not : term -> term,
     mk_map : typ -> typ -> term -> term -> term
   };
   val mk_monadT : compilation_funs -> typ -> typ
   val dest_monadT : compilation_funs -> typ -> typ
   val mk_empty : compilation_funs -> typ -> term
   val mk_single : compilation_funs -> term -> term
   val mk_bind : compilation_funs -> term * term -> term
   val mk_plus : compilation_funs -> term * term -> term
   val mk_if : compilation_funs -> term -> term
   val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
   val mk_not : compilation_funs -> term -> term
   val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
   val funT_of : compilation_funs -> mode -> typ -> typ
   (* Different compilations *)
   datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
     | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
   val is_depth_limited_compilation : compilation -> bool
   val string_of_compilation : compilation -> string
   val compilation_names : (string * compilation) list
   val non_random_compilations : compilation list
   val random_compilations : compilation list
   (* Different options for compiler *)
   datatype options = Options of {
     expected_modes : (string * mode list) option,
     proposed_modes : (string * mode list) list,
     proposed_names : ((string * mode) * string) list,
     show_steps : bool,
     show_proof_trace : bool,
     show_intermediate_results : bool,
     show_mode_inference : bool,
     show_modes : bool,
     show_compilation : bool,
     show_caught_failures : bool,
     show_invalid_clauses : bool,
     skip_proof : bool,
     no_topmost_reordering : bool,
     function_flattening : bool,
     fail_safe_function_flattening : bool,
     specialise : bool,
     no_higher_order_predicate : string list,
     inductify : bool,
     detect_switches : bool,
     smart_depth_limiting : bool,
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
   val proposed_modes : options -> string -> mode list option
   val proposed_names : options -> string -> mode -> string option
   val show_steps : options -> bool
   val show_proof_trace : options -> bool
   val show_intermediate_results : options -> bool
   val show_mode_inference : options -> bool
   val show_modes : options -> bool
   val show_compilation : options -> bool
   val show_caught_failures : options -> bool
   val show_invalid_clauses : options -> bool
   val skip_proof : options -> bool
   val no_topmost_reordering : options -> bool
   val function_flattening : options -> bool
   val fail_safe_function_flattening : options -> bool
   val specialise : options -> bool
   val no_higher_order_predicate : options -> string list
   val is_inductify : options -> bool
   val detect_switches : options -> bool
   val smart_depth_limiting : options -> bool
   val compilation : options -> compilation
   val default_options : options
   val bool_options : string list
   val print_step : options -> string -> unit
   (* conversions *)
   val imp_prems_conv : conv -> conv
   (* simple transformations *)
   val split_conjuncts_in_assms : Proof.context -> thm -> thm
   val dest_conjunct_prem : thm -> thm list
   val expand_tuples : theory -> thm -> thm
   val case_betapply : theory -> term -> term
   val eta_contract_ho_arguments : theory -> thm -> thm
   val remove_equalities : theory -> thm -> thm
   val remove_pointless_clauses : thm -> thm list
   val peephole_optimisation : theory -> thm -> thm option
   (* auxillary *)
   val unify_consts : theory -> term list -> term list -> (term list * term list)
   val mk_casesrule : Proof.context -> term -> thm list -> term
   val preprocess_intro : theory -> thm -> thm
 
   val define_quickcheck_predicate :
     term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
 end
 
 structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
 struct
 
 (* general functions *)
 
 fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
   | comb_option f (NONE, SOME x2) = SOME x2
   | comb_option f (SOME x1, NONE) = SOME x1
   | comb_option f (NONE, NONE) = NONE
 
 fun map2_optional f (x :: xs) (y :: ys) = f x (SOME y) :: (map2_optional f xs ys)
   | map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs [])
   | map2_optional f [] [] = []
 
 fun find_indices f xs =
   map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs)
 
 (* mode *)
 
 datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
 
 (* equality of instantiatedness with respect to equivalences:
   Pair Input Input == Input and Pair Output Output == Output *)
 fun eq_mode (Fun (m1, m2), Fun (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4)
   | eq_mode (Pair (m1, m2), Pair (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4)
   | eq_mode (Pair (m1, m2), Input) = eq_mode (m1, Input) andalso eq_mode (m2, Input)
   | eq_mode (Pair (m1, m2), Output) = eq_mode (m1, Output) andalso eq_mode (m2, Output)
   | eq_mode (Input, Pair (m1, m2)) = eq_mode (Input, m1) andalso eq_mode (Input, m2)
   | eq_mode (Output, Pair (m1, m2)) = eq_mode (Output, m1) andalso eq_mode (Output, m2)
   | eq_mode (Input, Input) = true
   | eq_mode (Output, Output) = true
   | eq_mode (Bool, Bool) = true
   | eq_mode _ = false
 
 fun mode_ord (Input, Output) = LESS
   | mode_ord (Output, Input) = GREATER
   | mode_ord (Input, Input) = EQUAL
   | mode_ord (Output, Output) = EQUAL
   | mode_ord (Bool, Bool) = EQUAL
   | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
   | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
 
 fun list_fun_mode [] = Bool
   | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
 
 (* name: binder_modes? *)
 fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
   | strip_fun_mode Bool = []
   | strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode"
 
 (* name: strip_fun_mode? *)
 fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
   | dest_fun_mode mode = [mode]
 
 fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
   | dest_tuple_mode _ = []
 
 fun all_modes_of_typ' (T as Type ("fun", _)) =
   let
     val (S, U) = strip_type T
   in
     if U = HOLogic.boolT then
       fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
         (map all_modes_of_typ' S) [Bool]
     else
       [Input, Output]
   end
   | all_modes_of_typ' (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
     map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
   | all_modes_of_typ' _ = [Input, Output]
 
 fun all_modes_of_typ (T as Type ("fun", _)) =
     let
       val (S, U) = strip_type T
     in
       if U = \<^typ>\<open>bool\<close> then
         fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
           (map all_modes_of_typ' S) [Bool]
       else
         raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
     end
   | all_modes_of_typ \<^typ>\<open>bool\<close> = [Bool]
   | all_modes_of_typ _ =
     raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
 
 fun all_smodes_of_typ (T as Type ("fun", _)) =
   let
     val (S, U) = strip_type T
     fun all_smodes (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
       map_product (curry Pair) (all_smodes T1) (all_smodes T2)
       | all_smodes _ = [Input, Output]
   in
     if U = HOLogic.boolT then
       fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
     else
       raise Fail "invalid type for predicate"
   end
 
 fun ho_arg_modes_of mode =
   let
     fun ho_arg_mode (m as Fun _) =  [m]
       | ho_arg_mode (Pair (m1, m2)) = ho_arg_mode m1 @ ho_arg_mode m2
       | ho_arg_mode _ = []
   in
     maps ho_arg_mode (strip_fun_mode mode)
   end
 
 fun ho_args_of mode ts =
   let
     fun ho_arg (Fun _) (SOME t) = [t]
       | ho_arg (Fun _) NONE = raise Fail "mode and term do not match"
       | ho_arg (Pair (m1, m2)) (SOME (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2)) =
           ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2)
       | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE
       | ho_arg _ _ = []
   in
     flat (map2_optional ho_arg (strip_fun_mode mode) ts)
   end
 
 fun ho_args_of_typ T ts =
   let
     fun ho_arg (T as Type ("fun", [_, _])) (SOME t) =
           if body_type T = \<^typ>\<open>bool\<close> then [t] else []
       | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match"
       | ho_arg (Type(\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2]))
          (SOME (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2)) =
           ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2)
       | ho_arg (Type(\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) NONE =
           ho_arg T1 NONE @ ho_arg T2 NONE
       | ho_arg _ _ = []
   in
     flat (map2_optional ho_arg (binder_types T) ts)
   end
 
 fun ho_argsT_of_typ Ts =
   let
     fun ho_arg (T as Type("fun", [_,_])) = if body_type T = \<^typ>\<open>bool\<close> then [T] else []
       | ho_arg (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
           ho_arg T1 @ ho_arg T2
       | ho_arg _ = []
   in
     maps ho_arg Ts
   end
 
 
 (* temporary function should be replaced by unsplit_input or so? *)
 fun replace_ho_args mode hoargs ts =
   let
     fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
       | replace (Pair (m1, m2), Const (\<^const_name>\<open>Pair\<close>, T) $ t1 $ t2) hoargs =
           let
             val (t1', hoargs') = replace (m1, t1) hoargs
             val (t2', hoargs'') = replace (m2, t2) hoargs'
           in
             (Const (\<^const_name>\<open>Pair\<close>, T) $ t1' $ t2', hoargs'')
           end
       | replace (_, t) hoargs = (t, hoargs)
   in
     fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs)
   end
 
 fun ho_argsT_of mode Ts =
   let
     fun ho_arg (Fun _) T = [T]
       | ho_arg (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
           ho_arg m1 T1 @ ho_arg m2 T2
       | ho_arg _ _ = []
   in
     flat (map2 ho_arg (strip_fun_mode mode) Ts)
   end
 
 (* splits mode and maps function to higher-order argument types *)
 fun split_map_mode f mode ts =
   let
     fun split_arg_mode' (m as Fun _) t = f m t
       | split_arg_mode' (Pair (m1, m2)) (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) =
         let
           val (i1, o1) = split_arg_mode' m1 t1
           val (i2, o2) = split_arg_mode' m2 t2
         in
           (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2))
         end
       | split_arg_mode' m t =
         if eq_mode (m, Input) then (SOME t, NONE)
         else if eq_mode (m, Output) then (NONE,  SOME t)
         else raise Fail "split_map_mode: mode and term do not match"
   in
     (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
   end
 
 (* splits mode and maps function to higher-order argument types *)
 fun split_map_modeT f mode Ts =
   let
     fun split_arg_mode' (m as Fun _) T = f m T
       | split_arg_mode' (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
         let
           val (i1, o1) = split_arg_mode' m1 T1
           val (i2, o2) = split_arg_mode' m2 T2
         in
           (comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2))
         end
       | split_arg_mode' Input T = (SOME T, NONE)
       | split_arg_mode' Output T = (NONE,  SOME T)
       | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
   in
     (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
   end
 
 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
 
 fun fold_map_aterms_prodT comb f (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) s =
       let
         val (x1, s') = fold_map_aterms_prodT comb f T1 s
         val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
       in
         (comb x1 x2, s'')
       end
   | fold_map_aterms_prodT _ f T s = f T s
 
 fun map_filter_prod f (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) =
       comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   | map_filter_prod f t = f t
 
 fun split_modeT mode Ts =
   let
     fun split_arg_mode (Fun _) _ = ([], [])
       | split_arg_mode (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
           let
             val (i1, o1) = split_arg_mode m1 T1
             val (i2, o2) = split_arg_mode m2 T2
           in
             (i1 @ i2, o1 @ o2)
           end
       | split_arg_mode Input T = ([T], [])
       | split_arg_mode Output T = ([], [T])
       | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
   in
     (apply2 flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   end
 
 fun string_of_mode mode =
   let
     fun string_of_mode1 Input = "i"
       | string_of_mode1 Output = "o"
       | string_of_mode1 Bool = "bool"
       | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")"
     and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^  string_of_mode2 m2
       | string_of_mode2 mode = string_of_mode1 mode
     and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2
       | string_of_mode3 mode = string_of_mode2 mode
   in string_of_mode3 mode end
 
 fun ascii_string_of_mode mode' =
   let
     fun ascii_string_of_mode' Input = "i"
       | ascii_string_of_mode' Output = "o"
       | ascii_string_of_mode' Bool = "b"
       | ascii_string_of_mode' (Pair (m1, m2)) =
           "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
       | ascii_string_of_mode' (Fun (m1, m2)) =
           "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
     and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
           ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
       | ascii_string_of_mode'_Fun Bool = "B"
       | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m
     and ascii_string_of_mode'_Pair (Pair (m1, m2)) =
           ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
       | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
   in ascii_string_of_mode'_Fun mode' end
 
 
 (* premises *)
 
 datatype indprem =
   Prem of term | Negprem of term | Sidecond of term | Generator of (string * typ)
 
 fun dest_indprem (Prem t) = t
   | dest_indprem (Negprem t) = t
   | dest_indprem (Sidecond t) = t
   | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
 
 fun map_indprem f (Prem t) = Prem (f t)
   | map_indprem f (Negprem t) = Negprem (f t)
   | map_indprem f (Sidecond t) = Sidecond (f t)
   | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
 
 
 (* general syntactic functions *)
 
 fun is_equationlike_term (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _) = true
   | is_equationlike_term
       (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
 
 val is_equationlike = is_equationlike_term o Thm.prop_of
 
 fun is_pred_equation_term (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ u $ v) =
       (fastype_of u = \<^typ>\<open>bool\<close>) andalso (fastype_of v = \<^typ>\<open>bool\<close>)
   | is_pred_equation_term _ = false
 
 val is_pred_equation = is_pred_equation_term o Thm.prop_of
 
 fun is_intro_term constname t =
   the_default false (try (fn t =>
     case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
       Const (c, _) => c = constname
     | _ => false) t)
 
 fun is_intro constname t = is_intro_term constname (Thm.prop_of t)
 
 fun is_predT (T as Type("fun", [_, _])) = (body_type T = \<^typ>\<open>bool\<close>)
   | is_predT _ = false
 
 fun lookup_constr ctxt =
   let
     val tab = Ctr_Sugar.ctr_sugars_of ctxt
       |> maps (map_filter (try dest_Const) o #ctrs)
       |> map (fn (c, T) => ((c, (fst o dest_Type o body_type) T), BNF_Util.num_binder_types T))
   in fn (c, T) =>
     case body_type T of
       Type (Tname, _) => AList.lookup (op =) tab (c, Tname)
     | _ => NONE
   end;
 
 fun is_constrt ctxt =
   let
     val lookup_constr = lookup_constr ctxt
     fun check t =
       (case strip_comb t of
         (Var _, []) => true
       | (Free _, []) => true
       | (Const cT, ts) =>
           (case lookup_constr cT of
             SOME i =>
               length ts = i andalso forall check ts
           | _ => false)
       | _ => false)
   in check end
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
 fun strip_ex (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (x, T, t)) =
       let
         val (xTs, t') = strip_ex t
       in
         ((x, T) :: xTs, t')
       end
   | strip_ex t = ([], t)
 
 fun focus_ex t nctxt =
   let
     val ((xs, Ts), t') = apfst split_list (strip_ex t)
     val (xs', nctxt') = fold_map Name.variant xs nctxt;
     val ps' = xs' ~~ Ts;
     val vs = map Free ps';
     val t'' = Term.subst_bounds (rev vs, t');
   in ((ps', t''), nctxt') end
 
 val strip_intro_concl =
   strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of
 
 
 (* introduction rule combinators *)
 
 fun map_atoms f intro =
   let
     val (literals, head) = Logic.strip_horn intro
     fun appl t =
       (case t of
         (\<^term>\<open>Not\<close> $ t') => HOLogic.mk_not (f t')
       | _ => f t)
   in
     Logic.list_implies
       (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
   end
 
 fun fold_atoms f intro s =
   let
     val (literals, _) = Logic.strip_horn intro
     fun appl t s =
       (case t of
         (\<^term>\<open>Not\<close> $ t') => f t' s
       | _ => f t s)
   in fold appl (map HOLogic.dest_Trueprop literals) s end
 
 fun fold_map_atoms f intro s =
   let
     val (literals, head) = Logic.strip_horn intro
     fun appl t s =
       (case t of
         (\<^term>\<open>Not\<close> $ t') => apfst HOLogic.mk_not (f t' s)
       | _ => f t s)
     val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   in
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
 
 fun map_filter_premises f intro =
   let
     val (premises, head) = Logic.strip_horn intro
   in
     Logic.list_implies (map_filter f premises, head)
   end
 
 fun maps_premises f intro =
   let
     val (premises, head) = Logic.strip_horn intro
   in
     Logic.list_implies (maps f premises, head)
   end
 
 fun map_concl f intro =
   let
     val (premises, head) = Logic.strip_horn intro
   in
     Logic.list_implies (premises, f head)
   end
 
 
 (* combinators to apply a function to all basic parts of nested products *)
 
 fun map_products f (Const (\<^const_name>\<open>Pair\<close>, T) $ t1 $ t2) =
   Const (\<^const_name>\<open>Pair\<close>, T) $ map_products f t1 $ map_products f t2
   | map_products f t = f t
 
 
 (* split theorems of case expressions *)
 
 fun prepare_split_thm ctxt split_thm =
     (split_thm RS @{thm iffD2})
     |> Local_Defs.unfold0 ctxt [@{thm atomize_conjL[symmetric]},
       @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
 
 fun find_split_thm thy (Const (name, _)) =
     Option.map #split (Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) name)
   | find_split_thm _ _ = NONE
 
 
 (* lifting term operations to theorems *)
 
 fun map_term thy f th =
   Skip_Proof.make_thm thy (f (Thm.prop_of th))
 
 (*
 fun equals_conv lhs_cv rhs_cv ct =
   case Thm.term_of ct of
     Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct
   | _ => error "equals_conv"
 *)
 
 
 (* Different compilations *)
 
 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
   | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
     Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
 
 fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
   | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
   | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
   | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
   | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
   | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
   | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS
   | negative_compilation_of c = c
 
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
   | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | compilation_for_polarity _ c = c
 
 fun is_depth_limited_compilation c =
   (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq) orelse
   (c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq)
 
 fun string_of_compilation c =
   (case c of
     Pred => ""
   | Random => "random"
   | Depth_Limited => "depth limited"
   | Depth_Limited_Random => "depth limited random"
   | DSeq => "dseq"
   | Annotated => "annotated"
   | Pos_Random_DSeq => "pos_random dseq"
   | Neg_Random_DSeq => "neg_random_dseq"
   | New_Pos_Random_DSeq => "new_pos_random dseq"
   | New_Neg_Random_DSeq => "new_neg_random_dseq"
   | Pos_Generator_DSeq => "pos_generator_dseq"
   | Neg_Generator_DSeq => "neg_generator_dseq"
   | Pos_Generator_CPS => "pos_generator_cps"
   | Neg_Generator_CPS => "neg_generator_cps")
 
 val compilation_names =
  [("pred", Pred),
   ("random", Random),
   ("depth_limited", Depth_Limited),
   ("depth_limited_random", Depth_Limited_Random),
   (*("annotated", Annotated),*)
   ("dseq", DSeq),
   ("random_dseq", Pos_Random_DSeq),
   ("new_random_dseq", New_Pos_Random_DSeq),
   ("generator_dseq", Pos_Generator_DSeq),
   ("generator_cps", Pos_Generator_CPS)]
 
 val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
 
 
 val random_compilations = [Random, Depth_Limited_Random,
   Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq,
   Pos_Generator_CPS, Neg_Generator_CPS]
 
 
 (* datastructures and setup for generic compilation *)
 
 datatype compilation_funs = CompilationFuns of {
   mk_monadT : typ -> typ,
   dest_monadT : typ -> typ,
   mk_empty : typ -> term,
   mk_single : term -> term,
   mk_bind : term * term -> term,
   mk_plus : term * term -> term,
   mk_if : term -> term,
   mk_iterate_upto : typ -> term * term * term -> term,
   mk_not : term -> term,
   mk_map : typ -> typ -> term -> term -> term
 }
 
 fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
 fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
 fun mk_empty (CompilationFuns funs) = #mk_empty funs
 fun mk_single (CompilationFuns funs) = #mk_single funs
 fun mk_bind (CompilationFuns funs) = #mk_bind funs
 fun mk_plus (CompilationFuns funs) = #mk_plus funs
 fun mk_if (CompilationFuns funs) = #mk_if funs
 fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 
 
 (** function types and names of different compilations **)
 
 fun funT_of compfuns mode T =
   let
     val Ts = binder_types T
     val (inTs, outTs) =
       split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
   in
     inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
   end
 
 
 (* Different options for compiler *)
 
 datatype options = Options of {
   expected_modes : (string * mode list) option,
   proposed_modes : (string * mode list) list,
   proposed_names : ((string * mode) * string) list,
   show_steps : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
   show_mode_inference : bool,
   show_modes : bool,
   show_compilation : bool,
   show_caught_failures : bool,
   show_invalid_clauses : bool,
   skip_proof : bool,
   no_topmost_reordering : bool,
   function_flattening : bool,
   specialise : bool,
   fail_safe_function_flattening : bool,
   no_higher_order_predicate : string list,
   inductify : bool,
   detect_switches : bool,
   smart_depth_limiting : bool,
   compilation : compilation
 }
 
 fun expected_modes (Options opt) = #expected_modes opt
 fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
 fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
   (#proposed_names opt) (name, mode)
 
 fun show_steps (Options opt) = #show_steps opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
 fun show_modes (Options opt) = #show_modes opt
 fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_compilation (Options opt) = #show_compilation opt
 fun show_caught_failures (Options opt) = #show_caught_failures opt
 fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt
 fun skip_proof (Options opt) = #skip_proof opt
 
 fun function_flattening (Options opt) = #function_flattening opt
 fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt
 fun specialise (Options opt) = #specialise opt
 fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt
 fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
 
 fun is_inductify (Options opt) = #inductify opt
 
 fun compilation (Options opt) = #compilation opt
 
 fun detect_switches (Options opt) = #detect_switches opt
 
 fun smart_depth_limiting (Options opt) = #smart_depth_limiting opt
 
 val default_options = Options {
   expected_modes = NONE,
   proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
   show_modes = false,
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
   show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = false,
   specialise = false,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
   inductify = false,
   detect_switches = true,
   smart_depth_limiting = false,
   compilation = Pred
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
   "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering",
   "smart_depth_limiting"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()
 
 
 (* simple transformations *)
 
 (** tuple processing **)
 
 fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
   | rewrite_args (arg::args) (pats, intro_t, ctxt) =
       (case HOLogic.strip_tupleT (fastype_of arg) of
         (_ :: _ :: _) =>
         let
           fun rewrite_arg'
                 (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ t2, Type (\<^type_name>\<open>Product_Type.prod\<close>, [_, T2]))
                 (args, (pats, intro_t, ctxt)) =
                 rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
             | rewrite_arg'
                 (t, Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) (args, (pats, intro_t, ctxt)) =
                 let
                   val thy = Proof_Context.theory_of ctxt
                   val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
                   val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
                   val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
                   val args' = map (Pattern.rewrite_term thy [pat] []) args
                 in
                   rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
                 end
             | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
           val (args', (pats, intro_t', ctxt')) =
             rewrite_arg' (arg, fastype_of arg) (args, (pats, intro_t, ctxt))
         in
           rewrite_args args' (pats, intro_t', ctxt')
         end
   | _ => rewrite_args args (pats, intro_t, ctxt))
 
 fun rewrite_prem atom =
   let
     val (_, args) = strip_comb atom
   in rewrite_args args end
 
 fun split_conjuncts_in_assms ctxt th =
   let
     val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
     fun split_conjs i nprems th =
       if i > nprems then th
       else
         (case try (op RSN) (@{thm conjI}, (i, th)) of
           SOME th' => split_conjs i (nprems + 1) th'
         | NONE => split_conjs (i + 1) nprems th)
   in
     singleton (Variable.export ctxt' ctxt)
       (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
   end
 
 fun dest_conjunct_prem th =
   (case HOLogic.dest_Trueprop (Thm.prop_of th) of
     (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _) =>
       dest_conjunct_prem (th RS @{thm conjunct1}) @
       dest_conjunct_prem (th RS @{thm conjunct2})
   | _ => [th])
 
 fun expand_tuples thy intro =
   let
     val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
     val intro_t = Thm.prop_of intro'
     val concl = Logic.strip_imp_concl intro_t
     val (_, args) = strip_comb (HOLogic.dest_Trueprop concl)
     val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
     val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
       (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
-    val t_insts' = map rewrite_pat t_insts
-    val intro'' = Thm.instantiate (T_insts, t_insts') intro
+    val t_insts' = map rewrite_pat (Term_Subst.Vars.dest t_insts)
+    val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' =
       Simplifier.full_simplify
         (put_simpset HOL_basic_ss ctxt
           addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])
       intro'''
     (* splitting conjunctions introduced by prod.inject*)
     val intro''''' = split_conjuncts_in_assms ctxt intro''''
   in
     intro'''''
   end
 
 
 (** making case distributivity rules **)
 (*** this should be part of the datatype package ***)
 
 fun datatype_name_of_case_name thy =
   Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy)
   #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type #> fst
 
 fun make_case_comb thy Tcon =
   let
     val ctxt = Proof_Context.init_global thy
     val SOME {casex, ...} = Ctr_Sugar.ctr_sugar_of ctxt Tcon
     val casex' = Type.legacy_freeze casex
     val Ts = BNF_Util.binder_fun_types (fastype_of casex')
   in
     list_comb (casex', map_index (fn (j, T) => Free ("f" ^ string_of_int j,  T)) Ts)
   end
 
 fun make_case_distrib thy Tcon =
   let
     val comb = make_case_comb thy Tcon;
     val Type ("fun", [T, T']) = fastype_of comb;
     val (Const (case_name, _), fs) = strip_comb comb
     val used = Term.add_tfree_names comb []
     val U = TFree (singleton (Name.variant_list used) "'t", \<^sort>\<open>type\<close>)
     val x = Free ("x", T)
     val f = Free ("f", T' --> U)
     fun apply_f f' =
       let
         val Ts = binder_types (fastype_of f')
         val bs = map Bound ((length Ts - 1) downto 0)
       in
         fold_rev absdummy Ts (f $ (list_comb (f', bs)))
       end
     val fs' = map apply_f fs
     val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   in
     HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
   end
 
 fun case_rewrite thy Tcon =
   (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
     (make_case_distrib thy Tcon)
 
 fun instantiated_case_rewrite thy Tcon =
   let
     val th = case_rewrite thy Tcon
     val ctxt = Proof_Context.init_global thy
     val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th)))))
     val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
     val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt
     val T' = TFree ("'t'", \<^sort>\<open>type\<close>)
     val U = TFree ("'u", \<^sort>\<open>type\<close>)
     val y = Free (yname, U)
     val f' = absdummy (U --> T') (Bound 0 $ y)
     val th' =
       Thm.instantiate
         ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
           (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
          [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
     val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
   in
     th'
   end
 
 fun case_betapply thy t =
   let
     val case_name = fst (dest_Const (fst (strip_comb t)))
     val Tcon = datatype_name_of_case_name thy case_name
     val th = instantiated_case_rewrite thy Tcon
   in
     Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
   end
 
 
 (*** conversions ***)
 
 fun imp_prems_conv cv ct =
   (case Thm.term_of ct of
     Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ =>
       Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   | _ => Conv.all_conv ct)
 
 
 (** eta contract higher-order arguments **)
 
 fun eta_contract_ho_arguments thy intro =
   let
     fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))
   in
     map_term thy (map_concl f o map_atoms f) intro
   end
 
 
 (** remove equalities **)
 
 fun remove_equalities thy intro =
   let
     fun remove_eqs intro_t =
       let
         val (prems, concl) = Logic.strip_horn intro_t
         fun remove_eq (prems, concl) =
           let
             fun removable_eq prem =
               (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
                 SOME (lhs, rhs) =>
                   (case lhs of
                     Var _ => true
                   | _ => (case rhs of Var _ => true | _ => false))
               | NONE => false)
           in
             (case find_first removable_eq prems of
               NONE => (prems, concl)
             | SOME eq =>
                 let
                   val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
                   val prems' = remove (op =) eq prems
                   val subst =
                     (case lhs of
                       (v as Var _) =>
                         (fn t => if t = v then rhs else t)
                     | _ => (case rhs of (v as Var _) => (fn t => if t = v then lhs else t)))
                 in
                   remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
                 end)
           end
       in
         Logic.list_implies (remove_eq (prems, concl))
       end
   in
     map_term thy remove_eqs intro
   end
 
 
 (* Some last processing *)
 
 fun remove_pointless_clauses intro =
   if Logic.strip_imp_prems (Thm.prop_of intro) = [\<^prop>\<open>False\<close>] then
     []
   else [intro]
 
 
 (* some peephole optimisations *)
 
 fun peephole_optimisation thy intro =
   let
     val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val process =
       rewrite_rule ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>code_pred_simp\<close>)
     fun process_False intro_t =
       if member (op =) (Logic.strip_imp_prems intro_t) \<^prop>\<open>False\<close>
       then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = \<^prop>\<open>True\<close> then NONE else SOME p) intro_t
   in
     Option.map (Skip_Proof.make_thm thy)
       (process_False (process_True (Thm.prop_of (process intro))))
   end
 
 
 (* importing introduction rules *)
 
 fun import_intros inp_pred [] ctxt =
       let
         val (outp_pred, ctxt') = yield_singleton (Variable.import_terms true) inp_pred ctxt
         val T = fastype_of outp_pred
         val paramTs = ho_argsT_of_typ (binder_types T)
         val (param_names, _) = Variable.variant_fixes
           (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
         val params = map2 (curry Free) param_names paramTs
       in
         (((outp_pred, params), []), ctxt')
       end
   | import_intros inp_pred (th :: ths) ctxt =
       let
         val ((_, [th']), ctxt') = Variable.import true [th] ctxt
         val thy = Proof_Context.theory_of ctxt'
         val (pred, args) = strip_intro_concl th'
         val T = fastype_of pred
         val ho_args = ho_args_of_typ T args
         fun subst_of (pred', pred) =
           let
             val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
               handle Type.TYPE_MATCH =>
                 error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
                   " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
                   " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
                   " in " ^ Thm.string_of_thm ctxt' th)
           in
             Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T))
               subst Term_Subst.TVars.empty
           end
         fun instantiate_typ th =
           let
             val (pred', _) = strip_intro_concl th
             val _ =
               if not (fst (dest_Const pred) = fst (dest_Const pred')) then
                 raise Fail "Trying to instantiate another predicate"
               else ()
             val instT =
               Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
                 (subst_of (pred', pred)) [];
           in Thm.instantiate (instT, []) th end
         fun instantiate_ho_args th =
           let
             val (_, args') =
               (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
             val ho_args' = map dest_Var (ho_args_of_typ T args')
           in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
         val outp_pred =
           Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred
         val ((_, ths'), ctxt1) =
           Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
       in
         (((outp_pred, ho_args), th' :: ths'), ctxt1)
       end
 
 
 (* generation of case rules from user-given introduction rules *)
 
 fun mk_args2 (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) st =
       let
         val (t1, st') = mk_args2 T1 st
         val (t2, st'') = mk_args2 T2 st'
       in
         (HOLogic.mk_prod (t1, t2), st'')
       end
   (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
     let
       val (S, U) = strip_type T
     in
       if U = HOLogic.boolT then
         (hd params, (tl params, ctxt))
       else
         let
           val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
         in
           (Free (x, T), (params, ctxt'))
         end
     end*)
   | mk_args2 T (params, ctxt) =
       let
         val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
       in
         (Free (x, T), (params, ctxt'))
       end
 
 fun mk_casesrule ctxt pred introrules =
   let
     (* TODO: can be simplified if parameters are not treated specially ? *)
     val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
     (* TODO: distinct required ? -- test case with more than one parameter! *)
     val params = distinct (op aconv) params
     val intros = map Thm.prop_of intros_th
     val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
     val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
     val argsT = binder_types (fastype_of pred)
     (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
     val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
     fun mk_case intro =
       let
         val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
         val prems = Logic.strip_imp_prems intro
         val eqprems =
           map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
         val frees = map Free (fold Term.add_frees (args @ prems) [])
       in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
     val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
     val cases = map mk_case intros
   in Logic.list_implies (assm :: cases, prop) end;
 
 
 (* unifying constants to have the same type variables *)
 
 fun unify_consts thy cs intr_ts =
   let
      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
      fun varify (t, (i, ts)) =
        let
          val t' = map_types (Logic.incr_tvar (i + 1))
            (#2 (Type.varify_global Term_Subst.TFrees.empty t))
        in (maxidx_of_term t', t' :: ts) end
      val (i, cs') = List.foldr varify (~1, []) cs
      val (i', intr_ts') = List.foldr varify (i, []) intr_ts
      val rec_consts = fold add_term_consts_2 cs' []
      val intr_consts = fold add_term_consts_2 intr_ts' []
      fun unify (cname, cT) =
        let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
        in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end
      val (env, _) = fold unify rec_consts (Vartab.empty, i')
      val subst = map_types (Envir.norm_type env)
    in (map subst cs', map subst intr_ts')
    end handle Type.TUNIFY =>
      (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts))
 
 
 (* preprocessing rules *)
 
 fun preprocess_equality thy rule =
   Conv.fconv_rule
     (imp_prems_conv
       (HOLogic.Trueprop_conv
         (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
     (Thm.transfer thy rule)
 
 fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
 
 
 (* defining a quickcheck predicate *)
 
 fun strip_imp_prems (Const(\<^const_name>\<open>HOL.implies\<close>, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
 fun strip_imp_concl (Const(\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ B) = strip_imp_concl B
   | strip_imp_concl A = A;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A)
 
 fun define_quickcheck_predicate t thy =
   let
     val (vs, t') = strip_abs t
     val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
     val t'' = subst_bounds (map Free (rev vs'), t')
     val (prems, concl) = strip_horn t''
     val constname = "quickcheck"
     val full_constname = Sign.full_bname thy constname
     val constT = map snd vs' ---> \<^typ>\<open>bool\<close>
     val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy
     val const = Const (full_constname, constT)
     val t =
       Logic.list_implies
         (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
           HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
     val intro =
       Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
         (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))
   in
     ((((full_constname, constT), vs'), intro), thy1)
   end
 
 end
diff --git a/src/Pure/Isar/subgoal.ML b/src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML
+++ b/src/Pure/Isar/subgoal.ML
@@ -1,257 +1,257 @@
 (*  Title:      Pure/Isar/subgoal.ML
     Author:     Makarius
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Tactical operations with explicit subgoal focus, based on canonical
 proof decomposition.  The "visible" part of the text within the
 context is fixed, the remaining goal may be schematic.
 
 Isar subgoal command for proof structure within unstructured proof
 scripts.
 *)
 
 signature SUBGOAL =
 sig
   type focus =
    {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
     concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
   val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
   val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
   val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
   val focus: Proof.context -> int -> binding list option -> thm -> focus * thm
   val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     int -> thm -> thm -> thm Seq.seq
   val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
   val subgoal: Attrib.binding -> Attrib.binding option ->
     bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
   val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
     bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
 end;
 
 structure Subgoal: SUBGOAL =
 struct
 
 (* focus *)
 
 type focus =
  {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
   concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
 
 fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
   let
     val st = raw_st
       |> Thm.solve_constraints
       |> Thm.transfer' ctxt
       |> Raw_Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
 
     val (asms, concl) =
       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
       else ([], goal);
     val text = asms @ (if do_concl then [concl] else []);
 
     val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
     val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
-    val schematics = (schematic_types, schematic_terms);
+    val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
     val concl' = Thm.instantiate_cterm schematics concl;
     val (prems, context) = Assumption.add_assumes asms' ctxt3;
   in
     ({context = context, params = params, prems = prems,
       asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
   end;
 
 val focus_params = gen_focus (false, false);
 val focus_params_fixed = gen_focus (false, true);
 val focus_prems = gen_focus (true, false);
 val focus = gen_focus (true, true);
 
 
 (* lift and retrofit *)
 
 (*
      B [?'b, ?y]
   ----------------
   B ['b, y params]
 *)
 fun lift_import idx params th ctxt =
   let
     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
 
     val Ts = map Thm.typ_of_cterm params;
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';
     val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
     val vars = build_rev (Term.add_vars prop);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
     fun var_inst v y =
       let
         val ((x, i), T) = v;
         val (U, args) =
           if Term_Subst.Vars.defined concl_vars v then (T, [])
           else (Ts ---> T, ts);
         val u = Free (y, U);
         in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
     val (inst1, inst2) =
       split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
 
     val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
   in ((inst2, th''), ctxt'') end;
 
 (*
        [x, A x]
           :
        B x \<Longrightarrow> C
   ------------------
   [\<And>x. A x \<Longrightarrow> B x]
           :
           C
 *)
 fun lift_subgoals ctxt params asms th =
   let
     fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct));
     val unlift =
       fold (Thm.elim_implies o Thm.assume) asms o
       Drule.forall_elim_list (map #2 params) o Thm.assume;
     val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
     val th' = fold (Thm.elim_implies o unlift) subgoals th;
   in (subgoals, th') end;
 
 fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
   let
     val idx = Thm.maxidx_of st0 + 1;
     val ps = map #2 params;
     val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
     val (subgoals, st3) = lift_subgoals ctxt2 params asms st2;
     val result = st3
       |> Goal.conclude
       |> Drule.implies_intr_list asms
       |> Drule.forall_intr_list ps
       |> Drule.implies_intr_list subgoals
       |> fold_rev (Thm.forall_intr o #1) subgoal_inst
       |> fold (Thm.forall_elim o #2) subgoal_inst
       |> Thm.adjust_maxidx_thm idx
       |> singleton (Variable.export ctxt2 ctxt0);
   in
     Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
       (false, result, Thm.nprems_of st1) i st0
   end;
 
 
 (* tacticals *)
 
 fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
     let val (args as {context = ctxt', params, asms, ...}, st') =
       gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st;
     in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
 
 val FOCUS_PARAMS = GEN_FOCUS (false, false);
 val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
 val FOCUS_PREMS = GEN_FOCUS (true, false);
 val FOCUS = GEN_FOCUS (true, true);
 
 fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
 
 
 (* Isar subgoal command *)
 
 local
 
 fun param_bindings ctxt (param_suffix, raw_param_specs) st =
   let
     val _ = if Thm.no_prems st then error "No subgoals!" else ();
     val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
     val subgoal_params =
       map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
       |> Term.variant_frees subgoal |> map #1;
 
     val n = length subgoal_params;
     val m = length raw_param_specs;
     val _ =
       m <= n orelse
         error ("Excessive subgoal parameter specification" ^
           Position.here_list (map snd (drop n raw_param_specs)));
 
     val param_specs =
       raw_param_specs |> map
         (fn (NONE, _) => NONE
           | (SOME x, pos) =>
               let
                 val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt));
                 val _ = Variable.check_name b;
               in SOME b end)
       |> param_suffix ? append (replicate (n - m) NONE);
 
     fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
       | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
       | bindings _ ys = map Binding.name ys;
   in bindings param_specs subgoal_params end;
 
 fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   let
     val _ = Proof.assert_backward state;
 
     val state1 = state |> Proof.refine_insert [];
     val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
 
     val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
     val (prems_binding, do_prems) =
       (case raw_prems_binding of
         SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
       | NONE => (Binding.empty_atts, false));
 
     val (subgoal_focus, _) =
       (if do_prems then focus else focus_params_fixed) ctxt
         1 (SOME (param_bindings ctxt param_specs st)) st;
 
     fun after_qed (ctxt'', [[result]]) =
       Proof.end_block #> (fn state' =>
         let
           val ctxt' = Proof.context_of state';
           val results' =
             Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
         in
           state'
           |> Proof.refine_primitive (fn _ => fn _ =>
             retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
               (Goal.protect 0 result) st
             |> Seq.hd)
           |> Proof.map_context
             (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
         end)
       #> Proof.reset_facts
       #> Proof.enter_backward;
   in
     state1
     |> Proof.enter_forward
     |> Proof.using_facts []
     |> Proof.begin_block
     |> Proof.map_context (fn _ =>
       #context subgoal_focus
       |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
     |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
         NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
     |> Proof.using_facts facts
     |> pair subgoal_focus
   end;
 
 in
 
 val subgoal = gen_subgoal Attrib.attribute;
 val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
 
 end;
 
 end;
 
 val SUBPROOF = Subgoal.SUBPROOF;
diff --git a/src/Pure/variable.ML b/src/Pure/variable.ML
--- a/src/Pure/variable.ML
+++ b/src/Pure/variable.ML
@@ -1,746 +1,745 @@
 (*  Title:      Pure/variable.ML
     Author:     Makarius
 
 Fixed type/term variables and polymorphic term abbreviations.
 *)
 
 signature VARIABLE =
 sig
   val names_of: Proof.context -> Name.context
   val binds_of: Proof.context -> (typ * term) Vartab.table
   val maxidx_of: Proof.context -> int
   val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
   val is_declared: Proof.context -> string -> bool
   val check_name: binding -> string
   val default_type: Proof.context -> string -> typ option
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
   val declare_maxidx: int -> Proof.context -> Proof.context
   val declare_names: term -> Proof.context -> Proof.context
   val declare_constraints: term -> Proof.context -> Proof.context
   val declare_internal: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
   val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
   val bind_term: indexname * term -> Proof.context -> Proof.context
   val unbind_term: indexname -> Proof.context -> Proof.context
   val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
   val declare_const: string * string -> Proof.context -> Proof.context
   val next_bound: string * typ -> Proof.context -> term * Proof.context
   val revert_bounds: Proof.context -> term -> term
   val is_body: Proof.context -> bool
   val set_body: bool -> Proof.context -> Proof.context
   val restore_body: Proof.context -> Proof.context -> Proof.context
   val improper_fixes: Proof.context -> Proof.context
   val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
   val is_improper: Proof.context -> string -> bool
   val is_fixed: Proof.context -> string -> bool
   val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
   val fixed_ord: Proof.context -> string ord
   val intern_fixed: Proof.context -> string -> string
   val lookup_fixed: Proof.context -> string -> string option
   val revert_fixed: Proof.context -> string -> string
   val markup_fixed: Proof.context -> string -> Markup.T
   val markup: Proof.context -> string -> Markup.T
   val markup_entity_def: Proof.context -> string -> Markup.T
   val dest_fixes: Proof.context -> (string * string) list
   val add_fixed_names: Proof.context -> term -> string list -> string list
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_newly_fixed: Proof.context -> Proof.context ->
     term -> (string * typ) list -> (string * typ) list
   val add_free_names: Proof.context -> term -> string list -> string list
   val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
   val add_fixes_implicit: term -> Proof.context -> Proof.context
   val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val gen_all: Proof.context -> thm -> thm
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
   val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
     (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context ->
-    (((indexname * sort) * ctyp) list * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
+    ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val is_bound_focus: Proof.context -> bool
   val set_bound_focus: bool -> Proof.context -> Proof.context
   val restore_bound_focus: Proof.context -> Proof.context -> Proof.context
   val focus_params: binding list option -> term -> Proof.context ->
     (string list * (string * typ) list) * Proof.context
   val focus: binding list option -> term -> Proof.context ->
     ((string * (string * typ)) list * term) * Proof.context
   val focus_cterm: binding list option -> cterm -> Proof.context ->
     ((string * cterm) list * cterm) * Proof.context
   val focus_subgoal: binding list option -> int -> thm -> Proof.context ->
     ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
   val polymorphic: Proof.context -> term list -> term list
 end;
 
 structure Variable: VARIABLE =
 struct
 
 (** local context data **)
 
 type fixes = (string * bool) Name_Space.table;
 val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
 
 datatype data = Data of
  {names: Name.context,                  (*type/term variable names*)
   consts: string Symtab.table,          (*consts within the local scope*)
   bounds: int * ((string * typ) * string) list,  (*next index, internal name, type, external name*)
   fixes: fixes,                         (*term fixes -- global name space, intern ~> extern*)
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
   maxidx: int,                          (*maximum var index*)
   constraints:
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
 
 fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =
   Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds,
     type_occs = type_occs, maxidx = maxidx, constraints = constraints};
 
 val empty_data =
   make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
     Symtab.empty, ~1, (Vartab.empty, Vartab.empty));
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init _ = empty_data;
 );
 
 fun map_data f =
   Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} =>
     make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)));
 
 fun map_names f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_consts f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_bounds f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_fixes f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints));
 
 fun map_binds f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints));
 
 fun map_type_occs f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints));
 
 fun map_maxidx f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints));
 
 fun map_constraints f =
   map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
     (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints));
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
 val fixes_space = Name_Space.space_of_table o fixes_of;
 val binds_of = #binds o rep_data;
 val type_occs_of = #type_occs o rep_data;
 val maxidx_of = #maxidx o rep_data;
 val constraints_of = #constraints o rep_data;
 
 val is_declared = Name.is_declared o names_of;
 
 val check_name = Name_Space.base_name o tap Binding.check;
 
 
 
 (** declarations **)
 
 (* default sorts and types *)
 
 fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1);
 
 fun def_type ctxt pattern xi =
   let val {binds, constraints = (types, _), ...} = rep_data ctxt in
     (case Vartab.lookup types xi of
       NONE =>
         if pattern then NONE
         else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1)
     | some => some)
   end;
 
 val def_sort = Vartab.lookup o #2 o constraints_of;
 
 
 (* maxidx *)
 
 val declare_maxidx = map_maxidx o Integer.max;
 
 
 (* names *)
 
 fun declare_type_names t =
   map_names (fold_types (fold_atyps Term.declare_typ_names) t) #>
   map_maxidx (fold_types Term.maxidx_typ t);
 
 fun declare_names t =
   declare_type_names t #>
   map_names (fold_aterms Term.declare_term_frees t) #>
   map_maxidx (Term.maxidx_term t);
 
 
 (* type occurrences *)
 
 fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T;
 
 val decl_type_occs = fold_term_types
   (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
     | _ => decl_type_occsT);
 
 val declare_type_occsT = map_type_occs o fold_types decl_type_occsT;
 val declare_type_occs = map_type_occs o decl_type_occs;
 
 
 (* constraints *)
 
 fun constrain_tvar (xi, raw_S) =
   let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
 
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let
     val types' = fold_aterms
       (fn Free (x, T) => Vartab.update ((x, ~1), T)
         | Var v => Vartab.update v
         | _ => I) t types;
     val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
         | TVar v => constrain_tvar v
         | _ => I) t sorts;
   in (types', sorts') end)
   #> declare_type_occsT t
   #> declare_type_names t;
 
 
 (* common declarations *)
 
 fun declare_internal t =
   declare_names t #>
   declare_type_occs t #>
   Thm.declare_term_sorts t;
 
 fun declare_term t =
   declare_internal t #>
   declare_constraints t;
 
 val declare_typ = declare_term o Logic.mk_type;
 
 val declare_prf =
   Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
 
 
 (* renaming term/type frees *)
 
 fun variant_frees ctxt ts frees =
   let
     val names = names_of (fold declare_names ts ctxt);
     val xs = fst (fold_map Name.variant (map #1 frees) names);
   in xs ~~ map snd frees end;
 
 
 
 (** term bindings **)
 
 fun bind_term ((x, i), t) =
   let
     val u = Term.close_schematic_term t;
     val U = Term.fastype_of u;
   in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
 
 val unbind_term = map_binds o Vartab.delete_safe;
 
 fun maybe_bind_term (xi, SOME t) = bind_term (xi, t)
   | maybe_bind_term (xi, NONE) = unbind_term xi;
 
 fun expand_binds ctxt =
   let
     val binds = binds_of ctxt;
     val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE;
   in Envir.beta_norm o Envir.expand_term get end;
 
 
 
 (** consts **)
 
 val lookup_const = Symtab.lookup o #consts o rep_data;
 val is_const = is_some oo lookup_const;
 
 val declare_fixed = map_consts o Symtab.delete_safe;
 val declare_const = map_consts o Symtab.update;
 
 
 
 (** bounds **)
 
 fun next_bound (a, T) ctxt =
   let
     val b = Name.bound (#1 (#bounds (rep_data ctxt)));
     val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
   in (Free (b, T), ctxt') end;
 
 fun revert_bounds ctxt t =
   (case #2 (#bounds (rep_data ctxt)) of
     [] => t
   | bounds =>
       let
         val names = Term.declare_term_names t (names_of ctxt);
         val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
         fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
       in Term.subst_atomic (map2 subst bounds xs) t end);
 
 
 
 (** fixes **)
 
 (* inner body mode *)
 
 val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false);
 val is_body = Config.apply inner_body;
 val set_body = Config.put inner_body;
 val restore_body = set_body o is_body;
 
 
 (* proper mode *)
 
 val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true);
 val improper_fixes = Config.put proper_fixes false;
 val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes;
 
 fun is_improper ctxt x =
   (case Name_Space.lookup (fixes_of ctxt) x of
     SOME (_, proper) => not proper
   | NONE => false);
 
 
 (* specialized name space *)
 
 val is_fixed = Name_Space.defined o fixes_of;
 fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
 
 fun lookup_fixed ctxt x =
   let val x' = intern_fixed ctxt x
   in if is_fixed ctxt x' then SOME x' else NONE end;
 
 fun revert_fixed ctxt x =
   (case Name_Space.lookup (fixes_of ctxt) x of
     SOME (x', _) => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
 fun markup_fixed ctxt x =
   Name_Space.markup (fixes_space ctxt) x
   |> Markup.name (revert_fixed ctxt x);
 
 fun markup ctxt x =
   if is_improper ctxt x then Markup.improper
   else if Name.is_skolem x then Markup.skolem
   else Markup.free;
 
 val markup_entity_def = Name_Space.markup_def o fixes_space;
 
 fun dest_fixes ctxt =
   Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) []
   |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2);
 
 
 (* collect variables *)
 
 fun add_free_names ctxt =
   fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I);
 
 fun add_frees ctxt =
   fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T) | _ => I);
 
 fun add_fixed_names ctxt =
   fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x | _ => I);
 
 fun add_fixed ctxt =
   fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I);
 
 fun add_newly_fixed ctxt' ctxt =
   fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I);
 
 
 (* declarations *)
 
 local
 
 fun err_dups dups =
   error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups));
 
 fun new_fixed ((x, x'), pos) ctxt =
   if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
   else
     let
       val proper = Config.get ctxt proper_fixes;
       val context = Context.Proof ctxt
         |> Name_Space.map_naming (K Name_Space.global_naming)
         |> Context_Position.set_visible_generic false;
     in
       ctxt
       |> map_fixes
         (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #>
           Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;
 
 fun new_fixes names' args =
   map_names (K names') #>
   fold new_fixed args #>
   pair (map (#2 o #1) args);
 
 in
 
 fun add_fixes_binding bs ctxt =
   let
     val _ =
       (case filter (Name.is_skolem o Binding.name_of) bs of
         [] => ()
       | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
     val _ =
       (case duplicates (op = o apply2 Binding.name_of) bs of
         [] => ()
       | dups => err_dups dups);
 
     val xs = map check_name bs;
     val names = names_of ctxt;
     val (xs', names') =
       if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
       else (xs, fold Name.declare xs names);
   in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end;
 
 fun variant_names ctxt raw_xs =
   let
     val names = names_of ctxt;
     val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
     val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
   in (names', xs ~~ xs') end;
 
 fun variant_fixes xs ctxt =
   let val (names', vs) = variant_names ctxt xs;
   in ctxt |> new_fixes names' (map (rpair Position.none) vs) end;
 
 fun bound_fixes xs ctxt =
   let
     val (names', vs) = variant_names ctxt (map #1 xs);
     val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt;
     val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys;
   in ctxt' |> new_fixes names' fixes end;
 
 end;
 
 val add_fixes = add_fixes_binding o map Binding.name;
 
 fun add_fixes_direct xs ctxt = ctxt
   |> set_body false
   |> (snd o add_fixes xs)
   |> restore_body ctxt;
 
 fun add_fixes_implicit t ctxt = ctxt
   |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []));
 
 
 (* dummy patterns *)
 
 fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt =
       let val ([x], ctxt') = ctxt |> set_body true |> add_fixes [Name.uu_] ||> restore_body ctxt
       in (Free (x, T), ctxt') end
   | fix_dummy_patterns (Abs (x, T, b)) ctxt =
       let val (b', ctxt') = fix_dummy_patterns b ctxt
       in (Abs (x, T, b'), ctxt') end
   | fix_dummy_patterns (t $ u) ctxt =
       let
         val (t', ctxt') = fix_dummy_patterns t ctxt;
         val (u', ctxt'') = fix_dummy_patterns u ctxt';
       in (t' $ u', ctxt'') end
   | fix_dummy_patterns a ctxt = (a, ctxt);
 
 
 
 (** export -- generalize type/term variables (beware of closure sizes) **)
 
 fun gen_all ctxt th =
   let
     val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1;
     fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T)));
   in fold gen (Drule.outer_params (Thm.prop_of th)) th end;
 
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
       Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
         not (is_fixed outer y) ? Symtab.insert_set y));
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
       Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
         then I else Symtab.insert_set a));
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
 
 fun exportT_terms inner outer =
   let
     val mk_tfrees = exportT_inst inner outer;
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
       (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
         (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
   end;
 
 fun export_terms inner outer =
   let
     val (mk_tfrees, tfrees) = export_inst inner outer;
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
       (Term_Subst.generalize (mk_tfrees ts, tfrees)
         (fold Term.maxidx_term ts maxidx + 1))
   end;
 
 fun export_prf inner outer prf =
   let
     val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
     val tfrees = mk_tfrees [];
     val maxidx = maxidx_of outer;
     val idx = Proofterm.maxidx_proof prf maxidx + 1;
     val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
     val gen_typ = Term_Subst.generalizeT_same tfrees idx;
   in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
 
 
 fun gen_export (mk_tfrees, frees) maxidx ths =
   let
     val tfrees = mk_tfrees (map Thm.full_prop_of ths);
     val idx = fold Thm.maxidx_thm ths maxidx + 1;
   in map (Thm.generalize (tfrees, frees) idx) ths end;
 
 fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
 
 fun export_morphism inner outer =
   let
     val fact = export inner outer;
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
   in
     Morphism.transfer_morphism' inner $>
     Morphism.transfer_morphism' outer $>
     Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
   end;
 
 
 
 (** import -- fix schematic type/term variables **)
 
 fun invent_types Ss ctxt =
   let
     val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
     val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   in (tfrees, ctxt') end;
 
 fun importT_inst ts ctxt =
   let
     val tvars = build_rev (fold Term.add_tvars ts);
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
     val instT =
       Term_Subst.TVars.build (fold2 (fn a => fn b =>
         Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
   in (instT, ctxt') end;
 
 fun import_inst is_open ts ctxt =
   let
     val ren = Name.clean #> (if is_open then I else Name.internal);
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
     val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst =
       Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
         Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
   in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
   in (map (Term_Subst.instantiate inst) ts, ctxt') end;
 
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val ths' = map (Thm.instantiate (instT', [])) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
   let
     val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []);
     val (insts, ctxt') = import_inst is_open ts ctxt;
   in (Proofterm.instantiate insts prf, ctxt') end;
 
 fun import is_open ths ctxt =
   let
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
-    val ths' = map (Thm.instantiate (instT', inst')) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
   in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =
   let val ((_, [th']), _) = ctxt |> set_body false |> import true [th];
   in th' end;
 
 
 (* import/export *)
 
 fun gen_trade imp exp f ctxt ths =
   let val ((_, ths'), ctxt') = imp ths ctxt
   in exp ctxt' ctxt (f ctxt' ths') end;
 
 val tradeT = gen_trade importT exportT;
 val trade = gen_trade (import true) export;
 
 
 (* focus on outermost parameters: \<And>x y z. B *)
 
 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
 val is_bound_focus = Config.apply bound_focus;
 val set_bound_focus = Config.put bound_focus;
 val restore_bound_focus = set_bound_focus o is_bound_focus;
 
 fun focus_params bindings t ctxt =
   let
     val ps = Term.variant_frees t (Term.strip_all_vars t);  (*as they are printed :-*)
     val (xs, Ts) = split_list ps;
     val (xs', ctxt') =
       (case bindings of
         SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt
       | NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt);
     val ps' = xs' ~~ Ts;
     val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps';
   in ((xs, ps'), ctxt'') end;
 
 fun focus bindings t ctxt =
   let
     val ((xs, ps), ctxt') = focus_params bindings t ctxt;
     val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
   in (((xs ~~ ps), t'), ctxt') end;
 
 fun forall_elim_prop t prop =
   Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
 fun focus_cterm bindings goal ctxt =
   let
     val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt;
     val ps' = map (Thm.cterm_of ctxt' o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
   in ((xs ~~ ps', goal'), ctxt') end;
 
 fun focus_subgoal bindings i st =
   let val all_vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars st) in
     Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
     Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
   end;
 
 
 
 (** implicit polymorphism **)
 
 (* warn_extra_tfrees *)
 
 fun warn_extra_tfrees ctxt1 ctxt2 =
   let
     fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false);
     fun occs_free a x =
       (case def_type ctxt1 false (x, ~1) of
         SOME T => if occs_typ a T then I else cons (a, x)
       | NONE => cons (a, x));
 
     val occs1 = type_occs_of ctxt1;
     val occs2 = type_occs_of ctxt2;
     val extras = Symtab.fold (fn (a, xs) =>
       if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 [];
     val tfrees = map #1 extras |> sort_distinct string_ord;
     val frees = map #2 extras |> sort_distinct string_ord;
   in
     if null extras orelse not (Context_Position.is_visible ctxt2) then ()
     else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
       space_implode " or " (map quote frees))
   end;
 
 
 (* polymorphic terms *)
 
 fun polymorphic_types ctxt ts =
   let
     val ctxt' = fold declare_term ts ctxt;
     val occs = type_occs_of ctxt;
     val occs' = type_occs_of ctxt';
     val types =
       Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
         if Symtab.defined occs a then I else Symtab.insert_set a));
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
           (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
         | _ => I) ts [];
     val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts;
   in (rev Ts', ts') end;
 
 fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
 
 end;