diff --git a/thys/ML_Unification/Binders/binders.ML b/thys/ML_Unification/Binders/binders.ML
--- a/thys/ML_Unification/Binders/binders.ML
+++ b/thys/ML_Unification/Binders/binders.ML
@@ -1,59 +1,57 @@
 (*  Title:      ML_Unification/binders.ML
     Author:     Kevin Kappelmann
 
 Binders with De Bruijn indexing.
 
 When we traverse abstractions, e.g. in unification algorithms, we store a binder as
 ((name, typ), fresh Free variable). The fresh free variable can be used as a replacement for
 the corresponding bound variable, e.g. when one has to create a reflexivity theorem for the
 binder.
 *)
 signature BINDERS =
 sig
   type 'a binder = (string * typ) * 'a
   type 'a binders = ('a binder) list
   (*add_binders bs1 bs2 adds binders bs1 to binders bs2*)
   val add_binders : 'a binders -> 'a binders -> 'a binders
   val fix_binders : (string * typ) list -> Proof.context -> term binders * Proof.context
   val fix_binder : (string * typ) -> Proof.context -> term binder * Proof.context
   (*returns types of binders*)
   val binder_types : 'a binders -> typ list
   (*returns free variable corresponding to the given binder*)
   val nth_binder_data : 'a binders -> int -> 'a
   (*replaces all binders by their corresponding free variable in the given term*)
   val replace_binders : term binders -> term -> term
   (*replaces all free variables that correspond to a binder by their binder*)
   val replace_frees : term binders -> term -> term
   (*normalises types and associated free variables*)
   val norm_binders : Term_Normalisation.term_normaliser -> term binders -> term binders
 end
 
 structure Binders : BINDERS =
 struct
 
 type 'a binder = (string * typ) * 'a
 type 'a binders = ('a binder) list
 
 fun add_binders binders1 binders2 = binders1 @ binders2
 
 fun fix_binders nTs ctxt =
   Variable.variant_fixes (map fst nTs) ctxt
   |>> map2 (fn (n, T) => fn n' => ((n, T), Free (n', T))) nTs
 
 val fix_binder = yield_singleton fix_binders
 
 fun binder_types binders = map (snd o fst) binders
 
 fun nth_binder_data binders = snd o nth binders
 
 fun replace_binders binders t = let val bvars = map snd binders
   in subst_bounds (bvars, t) end
 
-fun replace_frees binders =
-  let val subst = General_Util.fold_rev_index (fn (i, (_, free)) => cons (free, Bound i)) binders []
-  in subst_free subst end
+val replace_frees = fold_rev (curry abstract_over o snd)
 
 fun norm_binders norm =
   map (fn ((n, _), t) => let val t' = norm t in ((n, snd (dest_Free t')), t') end)
 
 end
diff --git a/thys/ML_Unification/Examples/E_Unification_Examples.thy b/thys/ML_Unification/Examples/E_Unification_Examples.thy
--- a/thys/ML_Unification/Examples/E_Unification_Examples.thy
+++ b/thys/ML_Unification/Examples/E_Unification_Examples.thy
@@ -1,163 +1,163 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>E-Unification Examples\<close>
 theory E_Unification_Examples
   imports
     Main
     ML_Unification_HOL_Setup
     Unify_Assumption_Tactic
     Unify_Fact_Tactic
     Unify_Resolve_Tactics
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Sample applications of e-unifiers, methods, etc. introduced in this session.\<close>
 
 experiment
 begin
 
 subsection \<open>Using The Simplifier For Unification.\<close>
 
 inductive_set even :: "nat set" where
 zero: "0 \<in> even" |
 step: "n \<in> even \<Longrightarrow> Suc (Suc n) \<in> even"
 
 text \<open>Premises of the form @{term "SIMPS_TO_UNIF lhs rhs"} are solved by
 @{ML_structure Simplifier_Unification}. It first normalises @{term lhs} and then unifies the
 normalisation with @{term rhs}. See also @{theory ML_Unification.ML_Unification_HOL_Setup}.\<close>
 
 lemma [uhint where prio = Prio.LOW]: "n \<noteq> 0 \<Longrightarrow> PROP SIMPS_TO_UNIF (n - 1) m \<Longrightarrow> n \<equiv> Suc m"
   unfolding SIMPS_TO_UNIF_eq by linarith
 
 text \<open>By default, below unification methods use
 @{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify}, which is a combination of
 various practical unification algorithms.\<close>
 
 schematic_goal "(\<And>x. x + 4 = n) \<Longrightarrow> Suc ?x = n"
   by uassm
 
 lemma "6 \<in> even"
   apply (urule step)
   apply (urule step)
   apply (urule step)
   apply (urule zero)
   done
 
 lemma "(220 + (80 - 2 * 2)) \<in> even"
   apply (urule step)
-  apply (urule step)+
+  apply (urule (rr) step)
   apply (urule zero)
   done
 
 lemma
   assumes "[a,b,c] = [c,b,a]"
   shows "[a] @ [b,c] = [c,b,a]"
   using assms by uassm
 
 lemma "x \<in> ({z, y, x} \<union> S) \<inter> {x}"
   by (ufact TrueI)
 
 schematic_goal "(x + (y :: nat))^2 \<le> x^2 + 2*x*y + y^2 + 4 * y + x - y"
   supply power2_sum[simp]
   by (ufact TrueI)
 
 lemma
   assumes "\<And>s. P (Suc (Suc 0)) (s(x := (1 :: nat), x := 1 + 1 * 4 - 3))"
   shows "P 2 (s(x := 2))"
   by (ufact assms)
 
 subsection \<open>Providing Canonical Solutions With Unification Hints\<close>
 
 lemma sub_self_eq_zero [uhint]: "(n :: nat) - n \<equiv> 0" by simp
 
 schematic_goal "n - ?m = (0 :: nat)"
   by (ufact refl)
 
 text \<open>The following example shows a non-trivial interplay of the simplifier and unification hints:
 Using just unification, the hint @{thm sub_self_eq_zero} is not applicable in the following example
 since @{term 0} cannot be unified with @{term "length []"}.
 However, the simplifier can rewrite @{term "length []"} to @{term 0} and the hint can then be applied.\<close>
 
 (*uncomment to see the trace*)
 declare [[ML_map_context \<open>Logger.set_log_levels Logger.root Logger.TRACE\<close>]]
 
 schematic_goal "n - ?m = length []"
   by (ufact refl)
 
 text \<open>There are also two ways to solve this using only unification hints:
 \<^enum> We allow the recursive use of unification hints when unifying @{thm sub_self_eq_zero} and our goal
 and register @{term "length [] = 0"} as an additional hint.
 \<^enum> We use an alternative for @{thm sub_self_eq_zero} that makes the recursive use of unification
 hints explicit and register @{term "length [] = 0"} as an additional hint.\<close>
 
 lemma length_nil_eq [uhint]: "length [] = 0" by simp
 
 text \<open>Solution 1: we can use @{attribute rec_uhint} for recursive usages of hints.
 Warning: recursive hint applications easily loop.\<close>
 
 schematic_goal "n - ?m = length []"
   supply [[ucombine del = \<open>(Standard_Unification_Combine.default_metadata \<^binding>\<open>simp_unif\<close>)\<close>]]
   (*doesn't work*)
   \<comment> \<open>by (ufact refl)\<close>
   supply sub_self_eq_zero[rec_uhint]
   by (ufact refl)
 
 text \<open>Solution 2: make the recursion explicit in the hint.\<close>
 
 lemma [uhint]: "k \<equiv> 0 \<Longrightarrow> (n :: nat) \<equiv> m \<Longrightarrow> n - m \<equiv> k" by simp
 
 schematic_goal "n - ?m = length []"
   supply [[ucombine del = \<open>(Standard_Unification_Combine.default_metadata \<^binding>\<open>simp_unif\<close>)\<close>]]
   by (ufact refl)
 
 subsection \<open>Strenghten Unification With Unification Hints\<close>
 
 lemma
   assumes [uhint]: "n = m"
   shows "n - m = (0 :: nat)"
   by (ufact refl)
 
 lemma
   assumes "x = y"
   shows "y = x"
   supply eq_commute[uhint]
   by (ufact assms)
 
 
 paragraph \<open>Unfolding definitions.\<close>
 
 definition "mysuc n = Suc n"
 
 lemma
   assumes "\<And>m. Suc n > mysuc m"
   shows "mysuc n > Suc 3"
   supply mysuc_def[uhint]
   by (ufact assms)
 
 
 paragraph \<open>Discharging meta impliciations with object-level implications\<close>
 
 lemma [uhint]:
   "Trueprop A \<equiv> A' \<Longrightarrow> Trueprop B \<equiv> B' \<Longrightarrow> Trueprop (A \<longrightarrow> B) \<equiv> (PROP A' \<Longrightarrow> PROP B')"
   using atomize_imp[symmetric] by simp
 
 lemma
   assumes "A \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> D"
   shows "A \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> D"
   using assms by ufact
 
 
 subsection \<open>Better Control Over Meta Variable Instantiations\<close>
 
 text \<open>Consider the following type-inference problem.\<close>
 schematic_goal
   assumes app_typeI: "\<And>f x.  (\<And>x. ArgT x \<Longrightarrow> DomT x (f x)) \<Longrightarrow> ArgT x \<Longrightarrow> DomT x (f x)"
   and f_type: "\<And>x. ArgT x \<Longrightarrow> DomT x (f x)"
   and x_type: "ArgT x"
   shows "?T (f x)"
   apply (urule app_typeI) \<comment>\<open>compare with the following application, creating an (unintuitive) higher-order instantiation\<close>
   (* apply (rule app_typeI) *)
   oops
 
 end
 
 end
diff --git a/thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy b/thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy
--- a/thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy
+++ b/thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy
@@ -1,216 +1,217 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 \<^marker>\<open>contributor "Paul Bachmann"\<close>
 section \<open>Examples: Reification Via Unification Hints\<close>
 theory Unification_Hints_Reification_Examples
   imports
     HOL.Rat
     ML_Unification_HOL_Setup
     Unify_Fact_Tactic
     Unify_Resolve_Tactics
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Reification via unification hints. For an introduction to unification hints refer
 to \<^cite>\<open>"unif-hints"\<close>. We support a generalisation of unification hints as described
 in @{theory ML_Unification.ML_Unification_Hints}.\<close>
 
 subsection \<open>Setup\<close>
 
 text \<open>One-time setup to obtain a unifier with unification hints for the purpose of reification.
 We could also simply use the standard unification hints @{attribute uhint} and
 @{attribute rec_uhint}, but having separate instances is a cleaner approach.\<close>
 
 ML\<open>
   @{functor_instance struct_name = Reification_Unification_Hints
     and functor_name = Term_Index_Unification_Hints
     and id = \<open>"reify"\<close>
     and more_args = \<open>
       structure TI = Discrimination_Tree
       val init_args = {
         concl_unifier = NONE,
         prems_unifier = NONE,
         normalisers = SOME Higher_Order_Pattern_Unification.norms_unify,
         retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval
           TI.norm_term TI.unifiables),
         hint_preprocessor = SOME (Standard_Unification_Hints.get_hint_preprocessor
           (Context.the_generic_context ()))
       }\<close>}
   val reify_unify = Unification_Combinator.add_fallback_unifier
     (fn unif_theory =>
       Higher_Order_Pattern_Unification.e_unify Unification_Util.unify_types unif_theory unif_theory
       |> Type_Unification.e_unify Unification_Util.unify_types)
     (Reification_Unification_Hints.try_hints
-      |> Unification_Combinator.norm_unifier (#norm_term Higher_Order_Pattern_Unification.norms_unify))
+      |> Unification_Combinator.norm_unifier
+        (Unification_Util.inst_norm_term' Higher_Order_Pattern_Unification.norms_unify))
 \<close>
 local_setup \<open>Reification_Unification_Hints.setup_attribute NONE\<close>
 
 text \<open>Premises of hints should again be unified by the reification unifier.\<close>
 declare [[reify_uhint where prems_unifier = reify_unify]]
 
 subsection \<open>Formulas with Quantifiers and Environment\<close>
 
 text \<open>The following example is taken from HOL-Library.Reflection\_Examples. It is recommended
 to compare the approach presented here with the reflection tactic presented in said theory.\<close>
 
 datatype form =
   TrueF
 | FalseF
 | Less nat nat
 | And form form
 | Or form form
 | Neg form
 | ExQ form
 
 primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
 where
   "interp TrueF vs \<longleftrightarrow> True"
 | "interp FalseF vs \<longleftrightarrow> False"
 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
 | "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
 | "interp (ExQ f) vs \<longleftrightarrow> (\<exists>v. interp f (v # vs))"
 
 paragraph \<open>Reification with unification and recursive hint unification for conclusion\<close>
 
 text \<open>The following illustrates how to use the equations @{thm interp.simps} directly
 as unification hints for reification.\<close>
 
 experiment
 begin
 
 text \<open>Hints for list lookup.\<close>
 declare List.nth_Cons_Suc[reify_uhint where prio = Prio.LOW]
   and List.nth_Cons_0[reify_uhint]
 
 text \<open>Hints to reify formulas of type @{type bool} into formulas of type @{type form}.\<close>
 declare interp.simps[reify_uhint]
 
 text \<open>We have to allow the hint unifier to recursively look for hints during unification of
 the hint's conclusion.\<close>
 declare [[reify_uhint where concl_unifier = reify_unify]]
 
 (*uncomment the following to see the hint unification process*)
 (* declare [[ML_map_context \<open>Logger.set_log_levels Unification_Base.logger Logger.DEBUG\<close>]] *)
 
 schematic_goal
   "interp ?f (?vs :: ('a :: ord) list) = (\<exists>(x :: 'a). x < y \<and> \<not>(\<exists>(z :: 'a). v < z \<or> \<not>False))"
   by (ufact refl where unifier = reify_unify)
 
 text \<open>While this all works nicely if set up correctly, it can be rather difficult to
 understand and debug the recursive unification process for a hint's conclusion.
 In the next paragraph, we present an alternative that is closer to the examples presented
 in the original unification hints paper \<^cite>\<open>"unif-hints"\<close>.\<close>
 
 end
 
 paragraph \<open>Reification with matching without recursion for conclusion\<close>
 
 text \<open>We disallow the hint unifier to recursively look for hints while unifying the conclusion;
 instead, we only allow the hint unifier to match the hint's conclusion against the disagreement terms.\<close>
 declare [[reify_uhint where concl_unifier =
   \<open>Higher_Order_Pattern_Unification.match |> Type_Unification.e_match Unification_Util.match_types\<close>]]
 
 text \<open>However, this also means that we now have to write our hints such that the hint's
 conclusion can successfully be matched against the disagreement terms. In particular,
 the disagreement terms may still contain meta variables that we want to instantiate with the help
 of the unification hints. Essentially, a hint then describes a canonical instantiation for
 these meta variables.\<close>
 
 experiment
 begin
 
 lemma [reify_uhint where prio = Prio.LOW]:
   "n \<equiv> Suc n' \<Longrightarrow> vs \<equiv> v # vs' \<Longrightarrow> vs' ! n' \<equiv> x \<Longrightarrow> vs ! n \<equiv> x"
   by simp
 
 lemma [reify_uhint]: "n \<equiv> 0 \<Longrightarrow> vs \<equiv> x # vs' \<Longrightarrow> vs ! n \<equiv> x"
   by simp
 
 lemma [reify_uhint]:
   "\<lbrakk>e \<equiv> ExQ f; \<And>v. interp f (v # vs) \<equiv> P v\<rbrakk> \<Longrightarrow> interp e vs \<equiv> \<exists>v. P v"
   "\<lbrakk>e \<equiv> Less i j; x \<equiv> vs ! i; y \<equiv> vs ! j\<rbrakk> \<Longrightarrow> interp e vs \<equiv> x < y"
   "\<lbrakk>e \<equiv> And f1 f2; interp f1 vs \<equiv> r1; interp f2 vs \<equiv> r2\<rbrakk> \<Longrightarrow> interp e vs \<equiv> r1 \<and> r2"
   "\<lbrakk>e \<equiv> Or f1 f2; interp f1 vs \<equiv> r1; interp f2 vs \<equiv> r2\<rbrakk> \<Longrightarrow> interp e vs \<equiv> r1 \<or> r2"
   "e \<equiv> Neg f \<Longrightarrow> interp f vs \<equiv> r \<Longrightarrow> interp e vs \<equiv> \<not>r"
   "e \<equiv> TrueF \<Longrightarrow> interp e vs \<equiv> True"
   "e \<equiv> FalseF \<Longrightarrow> interp e vs \<equiv> False"
   by simp_all
 
 schematic_goal
   "interp ?f (?vs :: ('a :: ord) list) = (\<exists>(x :: 'a). x < y \<and> \<not>(\<exists>(z :: 'a). v < z \<or> \<not>False))"
   by (urule refl where unifier = reify_unify)
 
 end
 
 text \<open>The next examples are modification from \<^cite>\<open>"unif-hints"\<close>.\<close>
 
 subsection \<open>Simple Arithmetic\<close>
 
 datatype add_expr = Var int | Add add_expr add_expr
 
 fun eval_add_expr :: "add_expr \<Rightarrow> int" where
   "eval_add_expr (Var i) = i"
 | "eval_add_expr (Add ex1 ex2) = eval_add_expr ex1 + eval_add_expr ex2"
 
 lemma eval_add_expr_Var [reify_uhint where prio = Prio.LOW]:
   "e \<equiv> Var i \<Longrightarrow> eval_add_expr e \<equiv> i" by simp
 
 lemma eval_add_expr_add [reify_uhint]:
   "e \<equiv> Add e1 e2 \<Longrightarrow> eval_add_expr e1 \<equiv> m \<Longrightarrow> eval_add_expr e2 \<equiv> n \<Longrightarrow> eval_add_expr e \<equiv> m + n"
   by simp
 
 ML_command\<open>
   val t1 = Proof_Context.read_term_pattern @{context} "eval_add_expr ?e"
   val t2 = Proof_Context.read_term_pattern @{context} "1 + (2 + 7) :: int"
   val _ = Unification_Util.log_unif_results @{context} (t1, t2) (reify_unify [])
 \<close>
 
 schematic_goal "eval_add_expr ?e = (1 + (2 + 7) :: int)"
   by (urule refl where unifier = reify_unify)
 
 
 subsection \<open>Arithmetic with Environment\<close>
 
 datatype mul_expr =
   Unit
 | Var nat
 | Mul mul_expr mul_expr
 | Inv mul_expr
 
 fun eval_mul_expr :: "mul_expr \<times> rat list \<Rightarrow> rat" where
   "eval_mul_expr (Unit, \<Gamma>) = 1"
 | "eval_mul_expr (Var i, \<Gamma>) = \<Gamma> ! i"
 | "eval_mul_expr (Mul e1 e2, \<Gamma>) = eval_mul_expr (e1, \<Gamma>) * eval_mul_expr (e2, \<Gamma>)"
 | "eval_mul_expr (Inv e, \<Gamma>) = inverse (eval_mul_expr (e, \<Gamma>))"
 
 text \<open>Split @{term e} into an expression and an environment.\<close>
 lemma [reify_uhint where prio = Prio.VERY_LOW]:
   "e \<equiv> (e1, \<Gamma>) \<Longrightarrow> eval_mul_expr (e1, \<Gamma>) \<equiv> n \<Longrightarrow> eval_mul_expr e \<equiv> n"
   by simp
 
 text \<open>Hints for environment lookup.\<close>
 lemma [reify_uhint where prio = Prio.LOW]:
   "e \<equiv> Var (Suc p) \<Longrightarrow> \<Gamma> \<equiv> s # \<Delta> \<Longrightarrow> n \<equiv> eval_mul_expr (Var p, \<Delta>) \<Longrightarrow> eval_mul_expr (e, \<Gamma>) \<equiv> n"
   by simp
 
 lemma [reify_uhint]: "e \<equiv> Var 0 \<Longrightarrow> \<Gamma> \<equiv> n # \<Theta> \<Longrightarrow> eval_mul_expr (e, \<Gamma>) \<equiv> n"
   by simp
 
 lemma [reify_uhint]:
   "e1 \<equiv> Inv e2 \<Longrightarrow> n \<equiv> eval_mul_expr (e2, \<Gamma>) \<Longrightarrow> eval_mul_expr (e1, \<Gamma>) \<equiv> inverse n"
   "e \<equiv> Mul e1 e2 \<Longrightarrow> m \<equiv> eval_mul_expr (e1, \<Gamma>) \<Longrightarrow> n \<equiv> eval_mul_expr (e2, \<Gamma>) \<Longrightarrow>
     eval_mul_expr (e, \<Gamma>) \<equiv> m * n"
   "e \<equiv> Unit \<Longrightarrow> eval_mul_expr (e, \<Gamma>) \<equiv> 1"
   by simp_all
 
 ML_command\<open>
   val t1 = Proof_Context.read_term_pattern @{context} "eval_mul_expr ?e"
   val t2 = Proof_Context.read_term_pattern @{context} "1 * inverse 3 * 5 :: rat"
   val _ = Unification_Util.log_unif_results' 1 @{context} (t2, t1) (reify_unify [])
 \<close>
 
 schematic_goal "eval_mul_expr ?e = (1 * inverse 3 * 5 :: rat)"
   by (ufact refl where unifier = reify_unify)
 
 end
diff --git a/thys/ML_Unification/ML_Unification_Base.thy b/thys/ML_Unification/ML_Unification_Base.thy
--- a/thys/ML_Unification/ML_Unification_Base.thy
+++ b/thys/ML_Unification/ML_Unification_Base.thy
@@ -1,17 +1,18 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>ML Unification Basics\<close>
 theory ML_Unification_Base
   imports
     ML_Logger
     ML_Binders
     ML_Normalisations
     ML_Theorem_Utils
+    SpecCheck.SpecCheck_Show
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Basic definitions and utilities for unification algorithms.\<close>
 
 ML_file\<open>unification_base.ML\<close>
 ML_file\<open>unification_util.ML\<close>
 
 end
diff --git a/thys/ML_Unification/ML_Unification_HOL_Setup.thy b/thys/ML_Unification/ML_Unification_HOL_Setup.thy
--- a/thys/ML_Unification/ML_Unification_HOL_Setup.thy
+++ b/thys/ML_Unification/ML_Unification_HOL_Setup.thy
@@ -1,34 +1,36 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>Setup for HOL\<close>
 theory ML_Unification_HOL_Setup
   imports
     HOL.HOL
     ML_Unification_Hints
 begin
 
 lemma eq_eq_True: "P \<equiv> (P \<equiv> Trueprop True)" by standard+ simp_all
 declare [[uhint where hint_preprocessor = \<open>Unification_Hints_Base.obj_logic_hint_preprocessor
   @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})\<close>]]
 and [[rec_uhint where hint_preprocessor = \<open>Unification_Hints_Base.obj_logic_hint_preprocessor
   @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})\<close>]]
 
 lemma eq_TrueI: "PROP P \<Longrightarrow> PROP P \<equiv> Trueprop True" by (standard) simp
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Simplifier_Unification.SIMPS_TO_unify @{thm eq_TrueI}
   |> Unification_Combinator.norm_closed_unifier
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
   |> Unification_Combinator.unifier_from_closed_unifier
   |> K)
   (Standard_Unification_Combine.metadata \<^binding>\<open>SIMPS_TO_unif\<close> Prio.HIGH)\<close>]]
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Simplifier_Unification.simp_unify_progress Envir.aeconv
     (Simplifier_Unification.SIMPS_TO_UNIF_unify @{thm eq_TrueI})
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
     Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify
     Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
   |> K)
   (Standard_Unification_Combine.metadata \<^binding>\<open>SIMPS_TO_UNIF_unif\<close> Prio.HIGH)\<close>]]
 
 
 end
diff --git a/thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy b/thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy
--- a/thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy
+++ b/thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy
@@ -1,16 +1,15 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>ML Conversion Utils\<close>
 theory ML_Conversion_Utils
   imports
     Pure
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Utilities for conversions.\<close>
 
-
 lemma meta_eq_symmetric: "(A \<equiv> B) \<equiv> (B \<equiv> A)"
   by (rule equal_intr_rule) simp_all
 ML_file\<open>conversion_util.ML\<close>
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML b/thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML
--- a/thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML
+++ b/thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML
@@ -1,53 +1,49 @@
 (*  Title:      ML_Utils/conversion_util.ML
     Author:     Kevin Kappelmann
 
 Conversion utilities.
 *)
 signature CONVERSION_UTIL =
 sig
-  val move_prem_to_front_conv : int -> conv
-  val move_prems_to_front_conv : int list -> conv
-  val thm_conv : conv -> thm -> thm
+  val apply_thm_conv : conv -> thm -> thm
+  val apply_subgoal_conv : conv -> int -> thm -> thm
+
   val binop_conv : conv -> conv -> conv
   val lhs_conv : conv -> conv
   val rhs_conv : conv -> conv
   val repeat_forall_conv : (cterm list -> Proof.context -> conv) -> Proof.context -> conv
   val imp_conv : conv -> conv -> conv
   val symmetric_conv : conv
+  val eta_short_conv : conv
+  val beta_eta_short_conv : conv
 end
 
 structure Conversion_Util : CONVERSION_UTIL =
 struct
 
-fun move_prem_to_front_conv 1 = Conv.all_conv
-  | move_prem_to_front_conv i = Conv.implies_concl_conv (move_prem_to_front_conv (i - 1))
-    then_conv Conv.rewr_conv Drule.swap_prems_eq
+val apply_thm_conv = Conv.fconv_rule
+val apply_subgoal_conv = Conv.gconv_rule
 
-val move_prems_to_front_conv = sort (rev_order o int_ord)
-  #> map_index (op +)
-  #> map move_prem_to_front_conv
-  #> Conv.every_conv
-
-val thm_conv = Conv.fconv_rule
-
-fun binop_conv conv_lhs conv_rhs =
-  Conv.combination_conv (Conv.arg_conv conv_lhs) conv_rhs
+fun binop_conv conv_lhs conv_rhs = Conv.combination_conv (Conv.arg_conv conv_lhs) conv_rhs
 
 val lhs_conv = Conv.arg1_conv
 val rhs_conv = Conv.arg_conv
 
 fun repeat_forall_conv cv =
   let
     fun conv fs ctxt =
       Conv.forall_conv (fn (f, ctxt) => conv (f :: fs) ctxt) ctxt
       else_conv (cv fs ctxt)
   in conv [] end
 
 fun imp_conv cvprem cvconcl ct = (case try Thm.dest_implies ct of
     NONE => cvconcl ct
   | SOME (A, C) => Drule.imp_cong_rule (cvprem A) (imp_conv cvprem cvconcl C))
 
 fun symmetric_conv ceq = let val (cl, cr) = Thm.dest_equals ceq
   in Thm.instantiate' [SOME (Thm.ctyp_of_cterm cl)] [SOME cl, SOME cr] @{thm meta_eq_symmetric} end
 
+val eta_short_conv = Thm.eta_conversion
+val beta_eta_short_conv = Drule.beta_eta_conversion
+
 end
diff --git a/thys/ML_Unification/ML_Utils/General/general_util.ML b/thys/ML_Unification/ML_Utils/General/general_util.ML
--- a/thys/ML_Unification/ML_Utils/General/general_util.ML
+++ b/thys/ML_Unification/ML_Utils/General/general_util.ML
@@ -1,74 +1,68 @@
 (*  Title:      ML_Utils/general_util.ML
     Author:     Kevin Kappelmann
 
 General ML utilities.
 *)
 signature GENERAL_UTIL =
 sig
   val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
 
   val find_first_index : ('a -> bool) -> 'a list -> (int * 'a) option
   val find_indices : ('a -> bool) -> 'a list -> int list
 
   (*returns false if function throws an exception*)
   val try_bool : ('a -> bool) -> 'a -> bool
 
   (*lists*)
   val fold_rev_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
   (* sequences *)
   (*raises exception if sequence is empty and returns the sequence otherwise*)
   val seq_try : exn -> 'a Seq.seq -> 'a Seq.seq
   val seq_is_empty : 'a Seq.seq -> (bool * 'a Seq.seq)
   val seq_merge : 'a ord -> ('a Seq.seq * 'a Seq.seq) -> 'a Seq.seq
 
 end
 
 structure General_Util : GENERAL_UTIL =
 struct
 
 fun flip f x y = f y x
 
 fun find_first_index p = get_index (Option.filter p)
 
 fun find_indices p =
   let
     fun find_indices _ [] = []
       | find_indices i (x :: xs) = (p x ? cons i) (find_indices (i + 1) xs)
   in find_indices 0 end
 
 fun try_bool f = try f #> (Option.getOpt o rpair false)
 
 (*lists*)
-fun insert _ x [] = [x]
-  | insert ord x (y :: ys) = case ord (x, y) of
-      LESS => x :: y :: ys
-    | EQUAL => x :: y :: ys
-    | GREATER => y :: insert ord x ys
-
 fun fold_rev_index f =
   let fun fold_aux _ [] y = y
         | fold_aux i (x :: xs) y = f (i, x) (fold_aux (i + 1) xs y)
   in fold_aux 0 end
 
 (* sequences *)
-fun seq_try exn sq = case Seq.pull sq of
-    NONE => raise exn
-  | SOME v => Seq.make (fn () => SOME v)
-
 fun seq_is_empty sq = case Seq.pull sq of
     NONE => (true, Seq.empty)
   | SOME v => (false, Seq.make (fn () => SOME v))
 
+fun seq_try exn sq = case seq_is_empty sq of
+    (true, _) => raise exn
+  | (false, sq) => sq
+
 fun seq_merge ord (xq, yq) =
   Seq.make (fn () => (case Seq.pull xq of
       NONE => Seq.pull yq
     | SOME (x, xq') => case Seq.pull yq of
         NONE => Seq.pull xq
       | SOME (y, yq') => case ord (x, y) of
           LESS => SOME (x, seq_merge ord (xq', Seq.cons y yq'))
         | EQUAL => SOME (x, seq_merge ord (xq', Seq.cons y yq'))
         | GREATER => SOME (y, seq_merge ord (Seq.cons x xq', yq')))
   )
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy b/thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy
--- a/thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy
+++ b/thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy
@@ -1,11 +1,12 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Priorities\<close>
 theory ML_Priorities
   imports ML_Parsing_Utils
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Priorities for ML tactics.\<close>
 
 ML_file\<open>priority.ML\<close>
 
 end
diff --git a/thys/ML_Unification/ML_Utils/Priorities/priority.ML b/thys/ML_Unification/ML_Utils/Priorities/priority.ML
--- a/thys/ML_Unification/ML_Utils/Priorities/priority.ML
+++ b/thys/ML_Unification/ML_Utils/Priorities/priority.ML
@@ -1,39 +1,42 @@
+(*  Title:      ML_Utils/priority.ML
+    Author:     Kevin Kappelmann
+*)
 signature PRIO = sig
   type prio = int
 
   val VERY_LOW : prio
   val LOW : prio
   val MEDIUM : prio
   val HIGH : prio
   val VERY_HIGH : prio
 
   val eq : prio * prio -> bool
   val ord : prio ord
 
   structure Table : TABLE
 
   val parse : prio context_parser
   val pretty : prio -> Pretty.T
 
 end
 
 structure Prio : PRIO =
 struct
 
 type prio = int
 
 val VERY_LOW = ~2000
 val LOW = ~1000
 val MEDIUM = 0
 val HIGH = 1000
 val VERY_HIGH = 2000
 
 val eq = (op =)
 val ord = int_ord o swap
 
 structure Table = Table(type key = prio; val ord = ord)
 
 val pretty = Pretty.str o string_of_int
 val parse = Parse_Util.ML_int (K "priority may not be empty")
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
--- a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
+++ b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
@@ -1,266 +1,256 @@
 (*  Title:      ML_Utils/tactic_util.ML
     Author:     Kevin Kappelmann
 
 Tactic utilities.
 *)
 signature TACTIC_UTIL =
 sig
   include HAS_LOGGER
   (* tactic combinators*)
   val HEADGOAL : (int -> 'a) -> 'a
 
   val THEN : ('a -> 'b Seq.seq) * ('b -> 'c Seq.seq) -> 'a -> 'c Seq.seq
   val THEN' : ('a -> 'b -> 'c Seq.seq) * ('a -> 'c -> 'd Seq.seq) -> 'a -> 'b -> 'd Seq.seq
 
   val TRY' : ('a -> tactic) -> 'a -> tactic
 
   val EVERY_ARG : ('a -> tactic) -> 'a list -> tactic
   val EVERY_ARG' : ('a -> 'b -> tactic) -> 'a list -> 'b -> tactic
   val CONCAT : tactic list -> tactic
   val CONCAT' : ('a -> tactic) list -> 'a -> tactic
 
   val FOCUS_PARAMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_CTXT : (Proof.context -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_CTXT' : (Proof.context -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_FIXED' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PREMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
 
   val CSUBGOAL_DATA : (cterm -> 'a) -> ('a -> int -> tactic) -> int -> tactic
   val CSUBGOAL_STRIPPED : (cterm Binders.binders * (cterm list * cterm) -> 'a) ->
     ('a -> int -> tactic) -> int -> tactic
   val SUBGOAL_DATA : (term -> 'a) -> ('a -> int -> tactic) -> int -> tactic
   val SUBGOAL_STRIPPED : ((string * typ) list * (term list * term) -> 'a) ->
     ('a -> int -> tactic) -> int -> tactic
 
   (* tactics *)
   val insert_tac : thm list -> Proof.context -> int -> tactic
   (*thin_tac n i deletes nth premise of the ith subgoal*)
   val thin_tac : int -> int -> tactic
   val thin_tacs : int list -> int -> tactic
 
   val set_kernel_ho_unif_bounds : int -> int -> Proof.context -> Proof.context
   val silence_kernel_ho_bounds_exceeded : Proof.context -> Proof.context
   val safe_simp_tac : Proof.context -> int -> tactic
 
   (*nth_eq_assume_tac n i solves ith subgoal by assumption, without unification,
     preferring premise n*)
   val nth_eq_assume_tac : int -> int -> tactic
 
   (*resolution without lifting of premises and parameters*)
   val no_lift_biresolve_tac : bool -> thm -> int -> Proof.context -> int -> tactic
   val no_lift_resolve_tac : thm -> int -> Proof.context -> int -> tactic
   val no_lift_eresolve_tac : thm -> int -> Proof.context -> int -> tactic
 
   (*rewrite subgoal according to the given equality theorem "lhs \<equiv> subgoal"*)
-  val rewrite_subgoal_tac : thm -> Proof.context -> int -> tactic
+  val rewrite_subgoal_tac : thm -> int -> tactic
 
   (*creates equality theorem for a subgoal from an equality theorem for the subgoal's conclusion;
     fails if the equality theorem contains a tpair or implicit Assumption mentioning one of the bound variables*)
   val eq_subgoal_from_eq_concl : cterm Binders.binders -> cterm list -> thm -> Proof.context ->
     thm option
 
   (*rewrite a subgoal given an equality theorem and environment for the subgoal's conclusion*)
   val rewrite_subgoal_unif_concl : Envir_Normalisation.term_normaliser ->
-    Envir_Normalisation.thm_normaliser -> Envir_Normalisation.thm_normaliser ->
+    (int -> Envir_Normalisation.thm_normaliser) -> Envir_Normalisation.thm_normaliser ->
     term Binders.binders -> (Envir.env * thm) -> Proof.context -> int -> tactic
 
   (*protect premises starting from (and excluding) the given index in the specified subgoal*)
   val protect_tac : int -> Proof.context -> int -> tactic
   (*unprotect the subgoal*)
   val unprotect_tac : Proof.context -> int -> tactic
   (*protect, then apply tactic, then unprotect*)
   val protected_tac : int -> (int -> tactic) -> Proof.context -> int -> tactic
 
   (*focus on the specified subgoal, introducing only the specified list of premises
     as theorems in the focus*)
   val focus_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
     Proof.context -> int -> tactic
   (*focus_prems_tac and then deletes all focused premises*)
   val focus_delete_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
     Proof.context -> int -> tactic
 
   (*apply tactic to the specified subgoal, where the state is given as a cterm*)
   val apply_tac : (int -> tactic) -> int -> cterm -> thm Seq.seq
 
 end
 
 structure Tactic_Util : TACTIC_UTIL =
 struct
 
 val logger = Logger.setup_new_logger Logger.root "Tactic_Util"
 
 (* tactic combinators *)
 fun HEADGOAL f = f 1
 
 fun (tac1 THEN tac2) = Seq.THEN (tac1, tac2)
 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x
 
 fun TRY' tac =  tac ORELSE' K all_tac
 
 fun EVERY_ARG tac = EVERY o map tac
 fun EVERY_ARG' tac = EVERY' o map tac
 
 fun CONCAT tacs = fold_rev (curry op APPEND) tacs no_tac
 fun CONCAT' tacs = fold_rev (curry op APPEND') tacs (K no_tac)
 
 fun FOCUS_PARAMS' tac = Subgoal.FOCUS_PARAMS (HEADGOAL o tac)
 fun FOCUS_PARAMS_FIXED' tac = Subgoal.FOCUS_PARAMS_FIXED (HEADGOAL o tac)
 fun FOCUS_PREMS' tac = Subgoal.FOCUS_PREMS (HEADGOAL o tac)
 fun FOCUS' tac = Subgoal.FOCUS (HEADGOAL o tac)
 fun SUBPROOF' tac = Subgoal.SUBPROOF (HEADGOAL o tac)
 
 fun FOCUS_PARAMS_CTXT tac = Subgoal.FOCUS_PARAMS (#context #> tac)
 fun FOCUS_PARAMS_CTXT' tac = FOCUS_PARAMS' (#context #> tac)
 
 fun CSUBGOAL_DATA f tac = CSUBGOAL (uncurry tac o apfst f)
 fun CSUBGOAL_STRIPPED f = CSUBGOAL_DATA (f o Term_Util.strip_csubgoal)
 fun SUBGOAL_DATA f tac = SUBGOAL (uncurry tac o apfst f)
 fun SUBGOAL_STRIPPED f = SUBGOAL_DATA (f o Term_Util.strip_subgoal)
 
 (* tactics *)
 fun insert_tac thms ctxt = Method.insert_tac ctxt thms
 
 fun thin_tac n = if n < 1 then K no_tac
   else rotate_tac (n - 1) THEN' (DETERM o eresolve0_tac [thin_rl]) THEN' rotate_tac (~n + 1)
 val thin_tacs = sort int_ord
   #> map_index ((op -) o swap)
   #> EVERY_ARG' thin_tac
 
 fun set_kernel_ho_unif_bounds trace_bound search_bound =
   Config.put Unify.unify_trace_bound trace_bound
   #> Config.put Unify.search_bound search_bound
 
 val silence_kernel_ho_bounds_exceeded = Context_Position.set_visible false
 
 (*some "safe" solvers create instantiations via flex-flex pairs, which we disallow here*)
 fun safe_simp_tac ctxt i state =
   let
     val eq_flexps = Thm.tpairs_of
       #> pair (Thm.tpairs_of state)
       #> eq_list (eq_pair (op aconv) (op aconv))
     (*stop higher-order unifier from entering difficult unification problems*)
     val ctxt = set_kernel_ho_unif_bounds 1 1 ctxt |> silence_kernel_ho_bounds_exceeded
   in Simplifier.safe_simp_tac ctxt i state |> Seq.filter eq_flexps end
 
 fun nth_eq_assume_tac n = if n < 1 then K no_tac
   else rotate_tac (n - 1) THEN' eq_assume_tac
 
 (*resolution*)
 fun no_lift_biresolve_tac eres brule nsubgoals ctxt =
   Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
   (eres, brule, nsubgoals)
   #> PRIMSEQ
 
 val no_lift_resolve_tac = no_lift_biresolve_tac false
 val no_lift_eresolve_tac = no_lift_biresolve_tac true
 
-fun rewrite_subgoal_tac eq_thm =
-  let
-    val (lhs, rhs) = Thm.dest_equals (Thm.cconcl_of eq_thm)
-    val eq_elim = Thm.instantiate' [] [SOME lhs, SOME rhs] Drule.equal_elim_rule1
-    val thm = Thm.implies_elim eq_elim eq_thm
-  in no_lift_resolve_tac thm 1 end
+fun rewrite_subgoal_tac eq_thm = CONVERSION (K (Thm.symmetric eq_thm))
 
 fun eq_subgoal_from_eq_concl cbinders cprems eq_thm ctxt =
   let
     fun all_abstract ((x, T), cfree) =
       let val all_const = Logic.all_const T |> Thm.cterm_of ctxt
       in
         Thm_Util.abstract_rule ctxt x cfree
         #> Option.map (Drule.arg_cong_rule all_const)
       end
   in
     (*introduce the premises*)
     SOME (fold_rev (Drule.imp_cong_rule o Thm.reflexive) cprems eq_thm)
     (*introduce abstractions for the fresh Frees*)
     |> fold (Option.mapPartial o all_abstract) cbinders
   end
 
-fun rewrite_subgoal_unif_concl norm_binders norm_state norm_eq_thm binders (env_eq_thm as (env, _))
+fun rewrite_subgoal_unif_concl inst_binders norm_state norm_eq_thm binders (env_eq_thm as (env, _))
   ctxt i =
   let
     (*updates binders with their normalised type*)
-    fun updated_binders env = Binders.norm_binders (norm_binders env) binders
-    val binders = updated_binders env
-    fun smash_tpairs_if_occurs (_, bvar) =
-      Seq.maps (Unification_Util.smash_tpairs_if_occurs ctxt bvar)
+    fun normed_binders env = Binders.norm_binders (inst_binders env) binders
+    val binders = normed_binders env
+    val smash_tpairs_if_occurs = Seq.maps o Unification_Util.smash_tpairs_if_occurs ctxt
     fun rewrite_tac env eq_thm prems =
       let
-        val binders = updated_binders env
+        val binders = normed_binders env
         val cterm_of = Thm.cterm_of ctxt
         val cprems = map (cterm_of o Binders.replace_binders binders) prems
       in
         eq_subgoal_from_eq_concl (map (apsnd cterm_of) binders) cprems (norm_eq_thm ctxt env eq_thm)
           ctxt
-        |> Option.map (fn eq_thm => rewrite_subgoal_tac eq_thm ctxt)
+        |> Option.map rewrite_subgoal_tac
         |> the_default (K no_tac)
       end
   in
     (*smash tpairs in case some binder occurs*)
-    fold smash_tpairs_if_occurs binders (Seq.single env_eq_thm)
+    fold (smash_tpairs_if_occurs o snd) binders (Seq.single env_eq_thm)
     |> Seq.lifts (fn (env, eq_thm) =>
-      PRIMITIVE (norm_state ctxt env)
+      PRIMITIVE (norm_state i ctxt env)
       THEN SUBGOAL_STRIPPED (fst o snd) (rewrite_tac env eq_thm) i)
   end
 
 fun protect_tac n ctxt =
   let fun protect cbinders (cprems, cconcl) i =
     let val nprems = length cprems
     in
       if nprems < n then
         (@{log Logger.WARN} ctxt (fn _ => Pretty.block [
           Pretty.str "Not enough premises to protect. Given number: ",
           Pretty.str (string_of_int n),
           Pretty.str ". But there are only ",
           Pretty.str (string_of_int nprems),
           Pretty.str " premise(s) in subgoal ",
           Pretty.str (string_of_int i),
           Pretty.str ": ",
           Logic.close_prop (map (apfst fst o apsnd Thm.term_of) cbinders) (map Thm.term_of cprems)
             (Thm.term_of cconcl) |> Syntax.pretty_term ctxt
         ] |> Pretty.string_of);
         no_tac)
       else
         let
           val (cprems_unprotected, cconcl_protected) = chop n cprems
             ||> Drule.list_implies o rpair cconcl
         in
           @{thm Pure.prop_def}
           |> Thm.instantiate' [] [SOME cconcl_protected]
           |> (fn eq_thm => eq_subgoal_from_eq_concl cbinders cprems_unprotected eq_thm ctxt)
-          |> Option.map (fn protected_eq_thm => rewrite_subgoal_tac protected_eq_thm ctxt i)
+          |> Option.map (fn protected_eq_thm => rewrite_subgoal_tac protected_eq_thm i)
           |> the_default no_tac
         end
     end
   in if n < 0 then K no_tac else CSUBGOAL_STRIPPED I (uncurry protect) end
 
 fun unprotect_tac ctxt = match_tac ctxt [Drule.protectI]
 
 fun protected_tac n tac ctxt =
   protect_tac n ctxt
   THEN' tac
   THEN_ALL_NEW (unprotect_tac ctxt)
 
 fun focus_prems_tac is tac ctxt =
-  CONVERSION (Conversion_Util.move_prems_to_front_conv is)
+  K (PRIMITIVE (Drule.rearrange_prems is))
   THEN' protect_tac (length is) ctxt
   THEN' FOCUS_PREMS' (fn {context=ctxt, params=params, prems=prems,
-    asms=asms, concl=concl, schematics=schematics} =>
-    let val concl = Term_Util.unprotect concl
-    in
-      unprotect_tac ctxt
-      THEN' tac {context=ctxt, params=params, prems=prems, asms=asms, concl=concl,
-        schematics=schematics}
-    end
+    asms=asms, schematics=schematics, concl=concl} => unprotect_tac ctxt
+      THEN' tac {context=ctxt, params=params, prems=prems, asms=asms, schematics=schematics,
+        concl=Term_Util.unprotect concl}
   ) ctxt
 
 fun focus_delete_prems_tac is tac ctxt =
   focus_prems_tac is tac ctxt
   THEN' thin_tacs (1 upto length is)
 
 fun apply_tac tac i = Goal.init #> tac i #> Seq.map Goal.conclude
 
 end
 
diff --git a/thys/ML_Unification/ML_Utils/Terms/term_util.ML b/thys/ML_Unification/ML_Utils/Terms/term_util.ML
--- a/thys/ML_Unification/ML_Utils/Terms/term_util.ML
+++ b/thys/ML_Unification/ML_Utils/Terms/term_util.ML
@@ -1,95 +1,95 @@
 (*  Title:      ML_Utils/term_util.ML
     Author:     Kevin Kappelmann
 
 Term utilities.
 *)
 signature TERM_UTIL =
 sig
   val fresh_vars : string -> typ list -> int -> term list * int
   val fresh_var : string -> typ -> int -> term * int
 
   (*returns outer parameters in reversed order*)
   val strip_all : term -> (string * typ) list * term
   val strip_call : cterm -> cterm Binders.binders * cterm
 
   (*returns premises and conclusion*)
   val strip_imp : term -> term list * term
   val strip_cimp : cterm -> cterm list * cterm
 
   (*returns outer parameters in reversed order, premises, and conclusion*)
   val strip_subgoal : term -> (string * typ) list * (term list * term)
   val strip_csubgoal : cterm -> cterm Binders.binders * (cterm list * cterm)
   val strip_nth_subgoal : int -> thm -> (string * typ) list * (term list * term)
   val strip_nth_csubgoal : int -> thm -> cterm Binders.binders * (cterm list * cterm)
 
   (*replace outer parameters by fresh meta variables*)
   val forall_elim_vars : term -> int -> term * int
 
   val protect : cterm -> cterm
   val unprotect : cterm -> cterm
 
   val no_dummy_pattern : term -> bool
   val has_dummy_pattern : term -> bool
 end
 
 structure Term_Util : TERM_UTIL =
 struct
 
 fun fresh_vars name Ts idx =
   let fun mk_var_inc T i = (Var ((name, i + 1), T), (i + 1))
   in fold_map mk_var_inc Ts idx end
 
 fun fresh_var name = yield_singleton (fresh_vars name)
 
 val strip_all =
   let fun strip params (Const ("Pure.all", _) $ Abs (a, T, t)) = strip ((a, T) :: params) t
         | strip params t = (params, t)
   in strip [] end
 
 val strip_call =
   let fun strip params ct =
     ((let val (cp as (_, cx)) = Thm.dest_comb ct
     in case apply2 Thm.term_of cp of
         (Const ("Pure.all", _), Abs (a, T, _)) =>
           let val (cf, cb) = Thm.dest_abs_global cx
           in strip (((a, T), cf) :: params) cb end
       | _ => (params, ct)
     end)
     handle CTERM _ => (params, ct))
   in strip [] end
 
 fun strip_imp t =
   (let
     val (prem, t) = Logic.dest_implies t
     val (prems, concl) = strip_imp t
   in (prem :: prems, concl) end)
   handle TERM _ => ([], t)
 
 fun strip_cimp ct =
   (let
     val (cprem, ct) = Thm.dest_implies ct
     val (cprems, cconcl) = strip_cimp ct
   in (cprem :: cprems, cconcl) end)
   handle TERM _ => ([], ct)
 
 val strip_subgoal = strip_all ##> strip_imp
 val strip_csubgoal = strip_call ##> strip_cimp
 fun strip_nth_subgoal i = Thm.prop_of #> pair i #> Logic.nth_prem #> strip_subgoal
 fun strip_nth_csubgoal i state = Thm.cprem_of state i |> strip_csubgoal
 
 fun forall_elim_vars t i =
   let val (params, tbody) = strip_all t
   in
     if null params then (t, i)
     else
       fold_map (uncurry fresh_var) params i
       |>> Term.subst_bounds o rpair tbody
   end
 
 val protect = Drule.protect
 val unprotect = Thm.dest_arg
 
-val no_dummy_pattern = can (Term.no_dummy_patterns)
+val no_dummy_pattern = can Term.no_dummy_patterns
 val has_dummy_pattern = not o no_dummy_pattern
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML b/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML
--- a/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML
+++ b/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML
@@ -1,47 +1,39 @@
 (*  Title:      ML_Utils/thm_util.ML
     Author:     Kevin Kappelmann
 
 Theorem utilities.
 *)
 signature THM_UTIL =
 sig
   include HAS_LOGGER
 
   val pretty_THM : Proof.context -> string * int * thm list -> Pretty.T
 
-  (*fails if the equality theorem contains a tpair or implicit Assumption mentioning the bound variables*)
+  (*fails if the theorem contains a tpair or implicit Assumption mentioning the bound variable*)
   val abstract_rule : Proof.context -> string -> cterm -> thm -> thm option
-  (*"match_implies_elim prem thm" matches the first premise of thm against prem and then removes
-    the premise; without lifting*)
-  val match_implies_elim : thm -> thm -> thm
   val protect : thm -> thm
 end
 
 structure Thm_Util : THM_UTIL =
 struct
 
 val logger = Logger.setup_new_logger Logger.root "Thm_Util"
 
 fun pretty_THM ctxt (msg, subgoal, thms) = Pretty.block [
     Pretty.str msg,
     Pretty.fbrk,
     Pretty.str "Subgoal number ",
     Pretty.str (string_of_int subgoal),
     Pretty.fbrk,
     Pretty.str "Theorems ",
     Pretty.list "[" "]" (map (Thm.pretty_thm ctxt) thms)
   ]
 
 fun abstract_rule ctxt n ct thm = SOME (Thm.abstract_rule n ct thm)
   handle THM data => (@{log Logger.DEBUG} ctxt (fn _ => pretty_THM ctxt data |> Pretty.string_of);
     NONE)
 
-fun match_implies_elim prem thm =
-  Thm.instantiate (Thm.first_order_match (Thm.cprem_of thm 1, Thm.cprop_of prem)) thm
-  |> (fn thm => Thm.implies_elim thm prem)
-
-fun protect thm = Drule.protectI
-  |> Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), Thm.cprop_of thm)])
+fun protect thm = Thm.instantiate' [] [SOME (Thm.cprop_of thm)] Drule.protectI
   |> Thm.elim_implies thm
 
 end
diff --git a/thys/ML_Unification/Normalisations/ML_Normalisations.thy b/thys/ML_Unification/Normalisations/ML_Normalisations.thy
--- a/thys/ML_Unification/Normalisations/ML_Normalisations.thy
+++ b/thys/ML_Unification/Normalisations/ML_Normalisations.thy
@@ -1,14 +1,14 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>ML-Normalisations\<close>
 theory ML_Normalisations
   imports
-    Pure
+    ML_Conversion_Utils
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Normalisation functions for terms, types, and theorems.\<close>
 
 ML_file\<open>term_normalisation.ML\<close>
 ML_file\<open>envir_normalisation.ML\<close>
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/Normalisations/envir_normalisation.ML b/thys/ML_Unification/Normalisations/envir_normalisation.ML
--- a/thys/ML_Unification/Normalisations/envir_normalisation.ML
+++ b/thys/ML_Unification/Normalisations/envir_normalisation.ML
@@ -1,244 +1,211 @@
 (*  Title:      ML_Unification/envir_normalisation.ML
     Author:     Kevin Kappelmann
 
 Normalisations with respect to an environment. Adapted and generalised from envir.ML
 *)
 signature ENVIR_NORMALISATION =
 sig
   (* types *)
   type type_normaliser = Type.tyenv -> typ -> typ
   val norm_type_match : type_normaliser
   val norm_type_unif : type_normaliser
 
   (* terms *)
   type term_type_normaliser = Type.tyenv -> Term_Normalisation.term_normaliser
   val norm_term_types : type_normaliser -> term_type_normaliser
   type term_normaliser = Envir.env -> Term_Normalisation.term_normaliser
 
   (** matching **)
   val norm_term_types_match : term_type_normaliser
   (*without beta-normalisation*)
   val norm_term_match : term_normaliser
-  val eta_short_norm_term_match : term_normaliser
   (*with beta-normalisation*)
   val beta_norm_term_match : term_normaliser
-  val beta_eta_short_norm_term_match : term_normaliser
 
   (** unification **)
   val norm_term_types_unif : term_type_normaliser
   (*without beta-normalisation*)
   val norm_term_unif : term_normaliser
-  val eta_short_norm_term_unif : term_normaliser
   (*with beta-normalisation*)
   val beta_norm_term_unif : term_normaliser
-  val beta_eta_short_norm_term_unif : term_normaliser
 
   (* theorems *)
   type thm_normaliser = Proof.context -> Envir.env -> thm -> thm
   type thm_type_normaliser = thm_normaliser
 
   val norm_thm_types : type_normaliser -> thm_type_normaliser
   val norm_thm_types_match : thm_type_normaliser
   val norm_thm_types_unif : thm_type_normaliser
   val norm_thm : type_normaliser -> term_normaliser -> thm_normaliser
   val norm_thm_match : thm_normaliser
   val norm_thm_unif : thm_normaliser
-  val eta_short_norm_thm : type_normaliser -> term_normaliser -> thm_normaliser
-  val eta_short_norm_thm_match : thm_normaliser
-  val eta_short_norm_thm_unif : thm_normaliser
-  (*with beta-normalisation and eta-contraction*)
-  val beta_eta_short_norm_thm : type_normaliser -> term_normaliser -> thm_normaliser
-  val beta_eta_short_norm_thm_match : thm_normaliser
-  val beta_eta_short_norm_thm_unif : thm_normaliser
 
 end
 
 structure Envir_Normalisation : ENVIR_NORMALISATION =
 struct
 
 (* types *)
 type type_normaliser = Type.tyenv -> typ -> typ
 
 val norm_type_match = Envir.subst_type
 val norm_type_unif = Envir.norm_type
 
 (* terms *)
 type term_type_normaliser = Type.tyenv -> Term_Normalisation.term_normaliser
 fun norm_term_types norm_type = map_types o norm_type
 
 type term_normaliser = Envir.env -> Term_Normalisation.term_normaliser
 
 (** matching **)
 val norm_term_types_match = norm_term_types norm_type_match
 
 fun norm_abs_same2 normT norm (a, T, body) =
   Abs (a, normT T, Same.commit norm body)
   handle Same.SAME => Abs (a, T, norm body)
 
 fun norm_abs_comb_same beta_norm norm (abs_args as (_, _, body)) arg = if beta_norm
   then Same.commit norm (subst_bound (arg, body))
   else let val f = Abs abs_args
     in (norm f $ Same.commit norm arg handle Same.SAME => f $ norm arg) end
 
 fun norm_comb_same beta_norm norm f t = (case norm f of
     (nf as Abs (_, _, body)) => if beta_norm
       then Same.commit norm (subst_bound (t, body))
       else nf $ Same.commit norm t
   | nf => nf $ Same.commit norm t)
   handle Same.SAME => f $ norm t
 
 fun norm_term_match1 beta_norm tenv : term Same.operation =
   let
     fun norm (Var v) = (case Envir.lookup1 tenv v of
           SOME u => u
         | NONE => raise Same.SAME)
       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
       | norm (Abs abs_args $ t) = norm_abs_comb_same beta_norm norm abs_args t
       | norm (f $ t) = norm_comb_same beta_norm norm f t
       | norm _ = raise Same.SAME
   in norm end
 
 fun norm_term_match2 beta_norm (Envir.Envir {tenv, tyenv, ...}) : term Same.operation =
   let
     val normT = Envir.subst_type_same tyenv
     fun norm (Const (a, T)) = Const (a, normT T)
       | norm (Free (a, T)) = Free (a, normT T)
       | norm (v as Var (xi, T)) =
           let
             fun lookup v = (case Envir.lookup1 tenv (dest_Var v) of
                 SOME u => u
               | NONE => raise Same.SAME)
           in
             (normT T |> (fn T => Same.commit lookup (Var (xi, T))))
             handle Same.SAME => lookup v
           end
       | norm (Abs args) = norm_abs_same2 normT norm args
       | norm (Abs abs_args $ t) = norm_abs_comb_same beta_norm norm abs_args t
       | norm (f $ t) = norm_comb_same beta_norm norm f t
       | norm _ = raise Same.SAME
   in norm end
 
 fun norm_term_match_same beta_norm (envir as Envir.Envir {tenv, tyenv, ...}) =
   if Vartab.is_empty tyenv then norm_term_match1 beta_norm tenv
   else norm_term_match2 beta_norm envir
 
 fun norm_term_match env = Same.commit (norm_term_match_same false env)
 fun beta_norm_term_match env = Same.commit (norm_term_match_same true env)
-fun eta_short_norm_term_match env = norm_term_match env
-  #> Term_Normalisation.eta_short
-fun beta_eta_short_norm_term_match env = beta_norm_term_match env
-  #> Term_Normalisation.eta_short
 
 (** unification **)
 val norm_term_types_unif = norm_term_types norm_type_unif
 
 fun norm_type_unif_same tyenv : typ Same.operation =
   let
     fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
       | norm (TFree _) = raise Same.SAME
       | norm (TVar v) =
           (case Type.lookup tyenv v of
             SOME U => Same.commit norm U
           | NONE => raise Same.SAME)
   in norm end
 
 fun norm_term_unif1 beta_norm tenv : term Same.operation =
   let
     fun norm (Var v) = (case Envir.lookup1 tenv v of
           SOME u => Same.commit norm u
         | NONE => raise Same.SAME)
       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
       | norm (Abs abs_args $ t) = norm_abs_comb_same beta_norm norm abs_args t
       | norm (f $ t) = norm_comb_same beta_norm norm f t
       | norm _ = raise Same.SAME
   in norm end
 
 fun norm_term_unif2 beta_norm (envir as Envir.Envir {tyenv, ...}) : term Same.operation =
   let
     val normT = norm_type_unif_same tyenv
     fun norm (Const (a, T)) = Const (a, normT T)
       | norm (Free (a, T)) = Free (a, normT T)
       | norm (Var (xi, T)) = (case Envir.lookup envir (xi, T) of
           SOME u => Same.commit norm u
         | NONE => Var (xi, normT T))
       | norm (Abs args) = norm_abs_same2 normT norm args
       | norm (Abs abs_args $ t) = norm_abs_comb_same beta_norm norm abs_args t
       | norm (f $ t) = norm_comb_same beta_norm norm f t
       | norm _ = raise Same.SAME
   in norm end
 
 fun norm_term_unif_same beta_norm (envir as Envir.Envir {tenv, tyenv, ...}) =
   if Vartab.is_empty tyenv then norm_term_unif1 beta_norm tenv
   else norm_term_unif2 beta_norm envir
 
 fun norm_term_unif env = Same.commit (norm_term_unif_same false env)
 fun beta_norm_term_unif env = Same.commit (norm_term_unif_same true env)
-fun eta_short_norm_term_unif env = norm_term_unif env
-  #> Term_Normalisation.eta_short
-fun beta_eta_short_norm_term_unif env = beta_norm_term_unif env
-  #> Term_Normalisation.eta_short
 
 type thm_normaliser = Proof.context -> Envir.env -> thm -> thm
 type thm_type_normaliser = thm_normaliser
 
 (** theorems **)
 
 (*collect and normalise TVars of a term*)
 fun collect_norm_types norm_type ctxt tyenv t =
   let
     val norm_type' = norm_type tyenv
     fun prep_type_entry x = (x, Thm.ctyp_of ctxt (norm_type' (TVar x)))
   in
     fold_types (fold_atyps (fn TVar v => TVars.add (prep_type_entry v) | _ => I)) t
     |> TVars.build
   end
 
 (*collect and normalise Vars of a term*)
 fun collect_norm_terms norm_type norm_term ctxt (env as Envir.Envir {tyenv,...}) t =
   let
     val norm_type' = norm_type tyenv
     val norm_term' = norm_term env
     fun prep_term_entry (x as (n, T)) = ((n, norm_type' T), Thm.cterm_of ctxt (norm_term' (Var x)))
   in
     fold_aterms (fn Var v => Vars.add (prep_term_entry v) | _ => I) t
     |> Vars.build
   end
 
 (*normalise types of a theorem*)
 fun norm_thm_types norm_types ctxt (Envir.Envir {tyenv, ...}) thm =
   let
     val prop = Thm.full_prop_of thm
     val type_inst = collect_norm_types norm_types ctxt tyenv prop
     val inst = (type_inst, Vars.empty)
   in Thm.instantiate inst thm end
 
 val norm_thm_types_match = norm_thm_types norm_type_match
 val norm_thm_types_unif = norm_thm_types norm_type_unif
 
 (*normalise a theorem*)
 fun norm_thm norm_types norm_terms ctxt (env as Envir.Envir {tyenv,...}) thm =
   let
     val prop = Thm.full_prop_of thm
     val type_inst = collect_norm_types norm_types ctxt tyenv prop
     val term_inst = collect_norm_terms norm_types norm_terms ctxt env prop
     val inst = (type_inst, term_inst)
   in Thm.instantiate inst thm end
 
 val norm_thm_match = norm_thm norm_type_match norm_term_match
 val norm_thm_unif = norm_thm norm_type_unif norm_term_unif
 
-fun eta_short_norm_thm norm_types norm_terms ctxt env =
-  norm_thm norm_types norm_terms ctxt env
-  #> Conv.fconv_rule Thm.eta_conversion
-
-val eta_short_norm_thm_match = eta_short_norm_thm norm_type_match norm_term_match
-val eta_short_norm_thm_unif = eta_short_norm_thm norm_type_unif norm_term_unif
-
-fun beta_eta_short_norm_thm norm_types norm_terms ctxt env =
-  norm_thm norm_types norm_terms ctxt env
-  #> Conv.fconv_rule Drule.beta_eta_conversion
-
-val beta_eta_short_norm_thm_match = beta_eta_short_norm_thm norm_type_match norm_term_match
-val beta_eta_short_norm_thm_unif = beta_eta_short_norm_thm norm_type_unif norm_term_unif
-
 end
diff --git a/thys/ML_Unification/ROOT b/thys/ML_Unification/ROOT
--- a/thys/ML_Unification/ROOT
+++ b/thys/ML_Unification/ROOT
@@ -1,56 +1,57 @@
 chapter AFP
 
-session ML_Unification = "HOL" +
+session ML_Unification = "Pure" +
   description
     \<open>Various unification utilities for Isabelle/ML, e.g. E-unification, E-matching, and unification hints.\<close>
   options [timeout = 300]
   sessions
+    HOL
     SpecCheck
   directories
     "Binders"
     "Examples"
     "Logger"
     "Logger/Data_Structures"
     "ML_Utils"
     "ML_Utils/Attributes"
     "ML_Utils/Conversions"
     "ML_Utils/Functor_Instances"
     "ML_Utils/General"
     "ML_Utils/Generic_Data"
     "ML_Utils/Methods"
     "ML_Utils/ML_Attributes"
     "ML_Utils/ML_Code"
     "ML_Utils/Parsing"
     "ML_Utils/Priorities"
     "ML_Utils/Tactics"
     "ML_Utils/Terms"
     "ML_Utils/Theorems"
     "Normalisations"
     "Simps_To"
     "Term_Index"
     "Tests"
     "Unifiers"
     "Unification_Attributes"
     "Unification_Hints"
     "Unification_Parsers"
     "Unification_Tactics"
     "Unification_Tactics/Assumption"
     "Unification_Tactics/Fact"
     "Unification_Tactics/Resolution"
   theories
     ML_Logger
     ML_Logger_Examples
     ML_Utils
     ML_Unifiers
     Unification_Tactics
     Unification_Attributes
     ML_Unification_Hints
     ML_Unification_HOL_Setup
     E_Unification_Examples
     Unification_Hints_Reification_Examples
   theories [document = false]
     ML_Unification_Tests
   document_files
     "root.tex"
     "root.bib"
 
diff --git a/thys/ML_Unification/Simps_To/simps_to_unif.ML b/thys/ML_Unification/Simps_To/simps_to_unif.ML
--- a/thys/ML_Unification/Simps_To/simps_to_unif.ML
+++ b/thys/ML_Unification/Simps_To/simps_to_unif.ML
@@ -1,67 +1,70 @@
 (*  Title:      ML_Unification/simps_to_unif.ML
     Author:     Kevin Kappelmann
 
 Create SIMPS_TO_UNIF theorems.
 *)
 signature SIMPS_TO_UNIF =
 sig
   include HAS_LOGGER
 
   val dest_SIMPS_TO_UNIF : term -> (term * term)
   val cdest_SIMPS_TO_UNIF : cterm -> (cterm * cterm)
 
   val mk_SIMPS_TO_UNIF_cprop : cterm * cterm -> cterm
 
   val SIMPS_TO_UNIF_tac : (int -> tactic) -> (int -> thm -> 'a Seq.seq) -> Proof.context -> int ->
     thm -> 'a Seq.seq
 
   val SIMPS_TO_UNIF_env_thmsq : (int -> tactic) -> Unification_Base.normalisers ->
     Unification_Base.closed_unifier -> Proof.context -> term * term -> Envir.env ->
     (Envir.env * thm) Seq.seq
 end
 
 structure Simps_To_Unif : SIMPS_TO_UNIF =
 struct
 
 val logger = Logger.setup_new_logger simps_to_base_logger "Simps_To_Unif"
 
 val dest_SIMPS_TO_UNIF = \<^Const_fn>\<open>SIMPS_TO_UNIF _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>
 val cdest_SIMPS_TO_UNIF = Thm.dest_comb #>> Thm.dest_arg
 
 fun mk_SIMPS_TO_UNIF_cprop (clhs, crhs) = \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm clhs\<close>
   and clhs and crhs in cprop\<open>PROP (SIMPS_TO_UNIF clhs crhs)\<close> for clhs :: 'a\<close>
 
 fun SIMPS_TO_UNIF_tac simp_tac eq_tac ctxt =
   Tactic_Util.THEN' (
     match_tac ctxt [@{thm SIMPS_TO_UNIFI}]
     THEN' Simps_To.SIMPS_TO_tac (Simps_To.simp_inst_tac simp_tac) ctxt,
     eq_tac)
 
 fun SIMPS_TO_UNIF_env_thmsq simp_tac norms unif ctxt (tp as (lhs, rhs)) env =
   (let
     val goal = apply2 (Thm.cterm_of ctxt) tp |> mk_SIMPS_TO_UNIF_cprop |> Goal.init
     fun eq_tac i state =
       let
         val tp = Thm.cprem_of state i |> Thm.dest_equals |> apply2 Thm.term_of
-        fun norm_resolve (env, eq_thm) = #norm_unif_thm norms ctxt env eq_thm
-          |> Thm.implies_elim (#norm_thm norms ctxt env state)
+        val conv = #conv norms
+        fun norm_implies_elim (env, eq_thm) =
+          Unification_Util.inst_norm_thm (#inst_unif_thm norms) conv ctxt env eq_thm
+          |> Thm.implies_elim (Unification_Util.inst_norm_subgoal (#inst_thm norms) conv i ctxt env
+            state)
           |> pair env
-      in unif ctxt tp env |> Seq.map norm_resolve end
+      in unif ctxt tp env |> Seq.map norm_implies_elim end
   in
     (@{log Logger.TRACE} ctxt (fn _ => Pretty.block [
         Pretty.str "Creating ",
         Syntax.pretty_term ctxt @{term SIMPS_TO_UNIF},
         Pretty.str " theorems for ",
         Unification_Util.pretty_terms ctxt [lhs, rhs]
       ] |> Pretty.string_of);
     Tactic_Util.HEADGOAL (SIMPS_TO_UNIF_tac simp_tac eq_tac ctxt) goal
     |> Seq.map (apsnd Goal.conclude))
   end)
   handle TYPE _ => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
       Pretty.str "Types of terms ",
       Unification_Util.pretty_terms ctxt [lhs, rhs],
       Pretty.str " not equal"
     ] |> Pretty.string_of);
     Seq.empty)
 
 end
diff --git a/thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy b/thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy
--- a/thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy
+++ b/thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy
@@ -1,240 +1,241 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 \<^marker>\<open>contributor "Paul Bachmann"\<close>
 subsection \<open>First-Order ML Unification Tests\<close>
 theory First_Order_ML_Unification_Tests
   imports
     ML_Unification_Tests_Base
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Tests for @{ML_structure "First_Order_Unification"}.\<close>
 
 ML\<open>
   structure Prop = SpecCheck_Property
   structure UC = Unification_Combinator
+  structure UU = Unification_Util
   open Unification_Tests_Base
   structure Unif = First_Order_Unification
   structure Norm = Envir_Normalisation
   val match = Unif.match []
   val match_hints =
     let fun match binders =
       UC.add_fallback_matcher
-      (Unif.e_match Unification_Util.match_types)
+      (Unif.e_match UU.match_types)
       ((fn binders =>
         (Hints.map_retrieval (Hints.mk_retrieval Hints.TI.generalisations |> K)
         #> Hints.UH.map_concl_unifier (Higher_Order_Pattern_Unification.match
-          |> Type_Unification.e_match Unification_Util.match_types |> K)
-        #> Hints.UH.map_normalisers (Unification_Util.beta_eta_short_norms_match |> K)
+          |> Type_Unification.e_match UU.match_types |> K)
+        #> Hints.UH.map_normalisers (UU.beta_eta_short_norms_match |> K)
         #> Hints.UH.map_prems_unifier (match |> UC.norm_matcher Norm.beta_norm_term_match |> K))
         |> Context.proof_map
         #> Test_Unification_Hints.try_hints binders)
-        |> UC.norm_matcher (#norm_term Unif.norms_match))
+        |> UC.norm_matcher (UU.inst_norm_term' Unif.norms_match))
       binders
     in match [] end
 
   val unify = Unif.unify []
   val unify_hints =
     let fun unif binders =
       UC.add_fallback_unifier
-      (Unif.e_unify Unification_Util.unify_types)
+      (Unif.e_unify UU.unify_types)
       ((fn binders =>
         (Hints.UH.map_concl_unifier (Higher_Order_Pattern_Unification.match
-          |> Type_Unification.e_match Unification_Util.match_types |> K)
-        #> Hints.UH.map_normalisers (Unification_Util.beta_eta_short_norms_unif |> K)
+          |> Type_Unification.e_match UU.match_types |> K)
+        #> Hints.UH.map_normalisers (UU.beta_eta_short_norms_unif |> K)
         #> Hints.UH.map_prems_unifier (unif |> UC.norm_unifier Norm.beta_norm_term_unif |> K))
         |> Context.proof_map
         #> Test_Unification_Hints.try_hints binders)
-        |> UC.norm_unifier (#norm_term Unif.norms_unify))
+        |> UC.norm_unifier (UU.inst_norm_term' Unif.norms_unify))
       binders
     in unif [] end
 \<close>
 
 subsubsection \<open>Matching\<close>
 paragraph \<open>Unit Tests\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: nat \<Rightarrow> bool \<Rightarrow> nat"}
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("(?x :: nat \<Rightarrow> ?'Z) 1", "f 1"),
       ("?x :: nat", "(?x + 1 :: nat)"),
       ("(g :: nat \<Rightarrow> nat \<Rightarrow> nat) ?x ?x", "(g :: nat \<Rightarrow> nat \<Rightarrow> nat) (?x + 1) (?x + 1)"),
       ("\<lambda>y. (?x :: nat \<Rightarrow> ?'Z) y", "\<lambda>y. f y"),
       ("(g :: ?'X \<Rightarrow> ?'Y \<Rightarrow> ?'Z) (x :: ?'X) (y :: ?'Y)", "(g :: ?'Y \<Rightarrow> ?'Z \<Rightarrow> ?'Z) (x :: ?'Y) (y :: ?'Z)"),
       ("(g :: ?'Z \<Rightarrow> ?'X)", "\<lambda>(x :: ?'X). (g :: ?'X \<Rightarrow> ?'Y) x"),
       ("\<lambda> (x :: nat). (0 :: nat)", "\<lambda> (x :: nat). (0 :: nat)"),
       ("\<lambda> (x :: nat). x", "\<lambda> (x :: nat). x"),
       ("\<lambda> (x :: nat) (y :: bool). (x, y)", "\<lambda> (x :: nat) (y :: bool). (x, y)"),
       ("\<lambda> (x :: ?'A) (y :: bool). (?x :: ?'A \<Rightarrow> bool \<Rightarrow> ?'Z) x y", "\<lambda> (x :: nat) (y :: bool). f x y"),
       ("\<lambda>(x :: ?'X). (g :: ?'X \<Rightarrow> ?'X) x", "(g :: ?'X \<Rightarrow> ?'X)"),
       ("?g ?x ?y d", "g ?y ?x d"),
       ("f 0 True", "(\<lambda>x y. f y x) True 0"),
       ("\<lambda> (x :: ?'a) y. f y", "\<lambda>(x :: ?'b). f"),
       ("\<lambda>y z. (?x :: nat \<Rightarrow> bool \<Rightarrow> nat) y z", "f"),
       ("\<lambda>x. (?f :: nat \<Rightarrow> bool \<Rightarrow> nat) 0 x", "\<lambda>x. f 0 x")
     ]
     val check = check_unit_tests_hints_match tests true []
   in
     Lecker.test_group ctxt () [
       check "match" match,
       check "match_hints" match_hints
     ]
   end
 \<close>
 
 subparagraph \<open>Asymmetry\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: nat \<Rightarrow> bool \<Rightarrow> nat"}
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("f 1", "(?x :: nat \<Rightarrow> ?'Z) 1")
     ]
     val check = check_unit_tests_hints_match tests false []
   in
     Lecker.test_group ctxt () [
       check "match" match,
       check "match_hints" match_hints
     ]
   end
 \<close>
 
 subparagraph \<open>Ground Hints\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
     val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
       "?x \<equiv> 2 \<Longrightarrow> ?x + (-?x :: int) \<equiv> 0",
       "?x \<equiv> 0 \<Longrightarrow> ?y \<equiv> 0 \<Longrightarrow> (?x :: int) + ?y \<equiv> 0"
     ]
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("(2 + -2) + (0 + 0) :: int", "0 :: int")
     ]
     val check_hints = check_unit_tests_hints_match tests
   in
     Lecker.test_group ctxt () [
       check_hints false [] "match" match,
       check_hints false [] "match_hints without hints" match_hints,
       check_hints true hints "match_hints with hints" match_hints
     ]
   end
 \<close>
 
 
 subsubsection \<open>Unification\<close>
 paragraph \<open>Generated Tests\<close>
 
 ML_command\<open>
   structure Test_Params =
   struct
     val unify = unify
     val unify_hints = unify_hints
     val params = {
       nv = 4,
       ni = 2,
       max_h = 5,
       max_args = 4
     }
   end
   structure First_Order_Tests = First_Order_Unification_Tests(Test_Params)
   val _ = First_Order_Tests.tests @{context} (SpecCheck_Random.new ())
 \<close>
 
 paragraph \<open>Unit Tests\<close>
 subparagraph \<open>Occurs-Check\<close>
 
 ML_command\<open>
   let
     val unit_tests = [
       (
         Var (("x", 0), TVar (("X", 0), [])),
         Var (("y", 0), TVar (("X", 0), []) --> TFree ("'a", [])) $
           Var (("x", 0), TVar (("X", 0), []))
       ),
       (
         Var (("y", 0), TVar (("X", 0), []) --> TFree ("'a", [])) $
           Var (("x", 0), TVar (("X", 0), [])),
         Var (("x", 0), TVar (("X", 0), []))
       ),
       (
         Free (("f", [TVar (("X", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
           Var (("x", 0), TVar (("X", 0), [])) $
           Var (("y", 0), TVar (("X", 0), [])),
         Free (("f", [TVar (("X", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
           Var (("y", 0), TVar (("X", 0), [])) $ (
             Free (("g", TVar (("X", 0), []) --> TVar (("X", 0), []))) $
               Var (("x", 0), TVar (("X", 0), []))
           )
       ),
       (
         Free (("f", [TVar (("X", 0), []), TVar (("Y", 0), [])] ---> TFree ("'a", []))) $
           Var (("x", 0), TVar (("X", 0), [])) $
           Var (("y", 0), TVar (("Y", 0), [])),
         Free (("f", [TVar (("Y", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
           Var (("y", 0), TVar (("Y", 0), [])) $ (
             Free (("g", TVar (("X", 0), []) --> TVar (("X", 0), []))) $
               Var (("x", 0), TVar (("X", 0), []))
           )
       )
     ]
     fun check name unif ctxt _ =
       check_list unit_tests ("occurs-check for " ^ name)
         (Prop.prop (not o terms_unify_thms_correct_unif ctxt unif)) ctxt
       |> K ()
   in
     Lecker.test_group @{context} () [
       check "unify" unify,
       check "unify_hints" unify_hints
     ]
   end
 \<close>
 
 subparagraph \<open>Lambda-Abstractions\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: nat \<Rightarrow> bool \<Rightarrow> nat"}
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("\<lambda> (x :: nat). (0 :: nat)", "\<lambda> (x :: nat). (0 :: nat)"),
       ("\<lambda> (x :: nat). x", "\<lambda> (x :: nat). x"),
       ("\<lambda> (x :: nat) (y :: bool). (x, y)", "\<lambda> (x :: nat) (y :: bool). (x, y)"),
       ("\<lambda> (x :: ?'a) y. f y", "\<lambda>(x :: ?'b). f"),
       ("\<lambda> (x :: nat) (y :: bool). f x y", "\<lambda> (x :: nat) (y :: bool). (?x :: nat \<Rightarrow> bool \<Rightarrow> ?'Z) x y"),
       ("\<lambda>x. (?f :: nat \<Rightarrow> bool \<Rightarrow> nat) 0 x", "\<lambda>x. f ?g x"),
       ("(?f :: nat \<Rightarrow> bool \<Rightarrow> nat) (?n :: nat)", "?g :: bool \<Rightarrow> nat")
     ]
     val check = check_unit_tests_hints_unif tests true []
   in
     Lecker.test_group ctxt () [
       check "unify" unify,
       check "unify_hints" unify_hints
     ]
   end
 \<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
     val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
       "?x \<equiv> (0 :: nat) \<Longrightarrow> ?y \<equiv> ?z \<Longrightarrow> ?x + ?y \<equiv> ?z"
     ]
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("\<lambda> (x :: nat) (y :: bool). x", "\<lambda> (x :: nat) (y :: bool). 0 + x"),
       ("0 + (\<lambda> (x :: nat) (y :: bool). x) 0 ?y", "0 + (\<lambda> (x :: nat) (y :: bool). 0 + x) 0 ?z")
     ]
     val check_hints = check_unit_tests_hints_unif tests
   in
     Lecker.test_group ctxt () [
       check_hints false [] "unify" unify,
       check_hints false [] "unify_hints without hints" unify_hints,
       check_hints true hints "unify_hints with hints" unify_hints
     ]
   end
 \<close>
 
 
 end
diff --git a/thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy b/thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy
--- a/thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy
+++ b/thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy
@@ -1,192 +1,193 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 \<^marker>\<open>contributor "Paul Bachmann"\<close>
 subsection \<open>Higher-Order Pattern ML Unification Tests\<close>
 theory Higher_Order_Pattern_ML_Unification_Tests
   imports
     ML_Unification_Tests_Base
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Tests for @{ML_structure "Higher_Order_Pattern_Unification"}.\<close>
 
 ML\<open>
   structure Prop = SpecCheck_Property
   structure UC = Unification_Combinator
+  structure UU = Unification_Util
   open Unification_Tests_Base
   structure Unif = Higher_Order_Pattern_Unification
-  val norm_match_types = Type_Unification.e_match Unification_Util.match_types
+  val norm_match_types = Type_Unification.e_match UU.match_types
   val match = Unif.match |> norm_match_types
   val closed_match = match []
   val match_hints =
     let fun match binders =
       UC.add_fallback_matcher
-      (fn match_theory => Unif.e_match Unification_Util.match_types match_theory match_theory
+      (fn match_theory => Unif.e_match UU.match_types match_theory match_theory
         |> norm_match_types)
       ((fn binders =>
         (Hints.map_retrieval (Hints.mk_retrieval Hints.TI.generalisations |> K)
         #> Hints.UH.map_concl_unifier (match |> K)
         #> Hints.UH.map_normalisers (Unif.norms_match |> K)
         #> Hints.UH.map_prems_unifier (match |> K))
         |> Context.proof_map
         #> Test_Unification_Hints.try_hints binders)
-        |> UC.norm_matcher (#norm_term Unif.norms_match))
+        |> UC.norm_matcher (UU.inst_norm_term' Unif.norms_match))
       binders
     in match [] end
 
-  val norm_unif_types = Type_Unification.e_unify Unification_Util.unify_types
+  val norm_unif_types = Type_Unification.e_unify UU.unify_types
   val unify = Unif.unify |> norm_unif_types
   val closed_unify = unify []
   val unify_hints =
     let fun unif binders =
       UC.add_fallback_unifier
-      (fn unif_theory => Unif.e_unify Unification_Util.unify_types unif_theory unif_theory
+      (fn unif_theory => Unif.e_unify UU.unify_types unif_theory unif_theory
         |> norm_unif_types)
       ((fn binders =>
         (Hints.UH.map_concl_unifier (match |> K)
         #> Hints.UH.map_normalisers (Unif.norms_unify |> K)
         #> Hints.UH.map_prems_unifier (unif |> K))
         |> Context.proof_map
         #> Test_Unification_Hints.try_hints binders)
-        |> UC.norm_unifier (#norm_term Unif.norms_unify))
+        |> UC.norm_unifier (UU.inst_norm_term' Unif.norms_unify))
       binders
     in unif [] end
 \<close>
 
 subsubsection \<open>Matching\<close>
 paragraph \<open>Unit Tests\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: nat \<Rightarrow> bool \<Rightarrow> nat"}
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("?x :: nat", "(?x + 1 :: nat)"),
       ("(g :: nat \<Rightarrow> nat \<Rightarrow> nat) ?x ?x", "(g :: nat \<Rightarrow> nat \<Rightarrow> nat) (?x + 1) (?x + 1)"),
       ("\<lambda>y. (?x :: nat \<Rightarrow> ?'Z) y", "\<lambda>y. f y"),
       ("(g :: ?'X \<Rightarrow> ?'Y \<Rightarrow> ?'Z) (x :: ?'X) (y :: ?'Y)", "(g :: ?'Y \<Rightarrow> ?'Z \<Rightarrow> ?'Z) (x :: ?'Y) (y :: ?'Z)"),
       ("(g :: ?'Z \<Rightarrow> ?'X)", "\<lambda>(x :: ?'X). (g :: ?'X \<Rightarrow> ?'Y) x"),
       ("\<lambda> (x :: nat). (0 :: nat)", "\<lambda> (x :: nat). (0 :: nat)"),
       ("\<lambda> (x :: nat). x", "\<lambda> (x :: nat). x"),
       ("\<lambda> (x :: nat) (y :: bool). (x, y)", "\<lambda> (x :: nat) (y :: bool). (x, y)"),
       ("\<lambda> (x :: ?'A) (y :: bool). (?x :: ?'A \<Rightarrow> bool \<Rightarrow> ?'Z) x y", "\<lambda> (x :: nat) (y :: bool). f x y"),
       ("\<lambda>(x :: ?'X). (g :: ?'X \<Rightarrow> ?'X) x", "(g :: ?'X \<Rightarrow> ?'X)"),
       ("\<lambda>y. (?x :: nat \<Rightarrow> bool \<Rightarrow> nat) y", "\<lambda>y. f y"),
       ("\<lambda>y z. (?x :: nat \<Rightarrow> bool \<Rightarrow> nat) y z", "f")
     ]
     val check = check_unit_tests_hints_match tests true []
   in
     Lecker.test_group ctxt () [
       check "match" closed_match,
       check "match_hints" match_hints
     ]
   end
 \<close>
 
 subparagraph \<open>Asymmetry\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: nat \<Rightarrow> bool \<Rightarrow> nat"}
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("\<lambda>y. f y", "\<lambda>y. (?x :: nat \<Rightarrow> bool \<Rightarrow> nat) y")
     ]
     val check = check_unit_tests_hints_match tests false []
   in
     Lecker.test_group ctxt () [
       check "match" closed_match,
       check "match_hints" match_hints
     ]
   end
 \<close>
 
 subparagraph \<open>Ground Hints\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
     val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
       "?x \<equiv> 2 \<Longrightarrow> ?x + (-?x :: int) \<equiv> 0",
       "?x \<equiv> 0 \<Longrightarrow> ?y \<equiv> 0 \<Longrightarrow> (?x :: int) + ?y \<equiv> 0"
     ]
     val tests = map (apply2 (Syntax.read_term ctxt))[
       ("(2 + -2) + (0 + 0) :: int", "0 :: int")
     ]
     val check_hints = check_unit_tests_hints_match tests
   in
     Lecker.test_group ctxt () [
       check_hints false [] "match" closed_match,
       check_hints false [] "match_hints without hints" match_hints,
       check_hints true hints "match_hints with hints" match_hints
     ]
   end
 \<close>
 
 
 subsubsection \<open>Unification\<close>
 
 paragraph \<open>Generated Tests\<close>
 subparagraph \<open>First-Order\<close>
 
 ML_command\<open>
   structure Test_Params =
   struct
     val unify = closed_unify
     val unify_hints = unify_hints
     val params = {
       nv = 10,
       ni = 10,
       max_h = 5,
       max_args = 4
     }
   end
   structure First_Order_Tests = First_Order_Unification_Tests(Test_Params)
   val _ = First_Order_Tests.tests @{context} (SpecCheck_Random.new ())
 \<close>
 
 subparagraph \<open>Higher-Order Pattern\<close>
 
 ML_file\<open>higher_order_pattern_unification_tests.ML\<close>
 
 ML_command\<open>
   val ctxt = @{context}
   val tests = Higher_Order_Pattern_Unification_Tests.unit_tests_unifiable ctxt
   val check_hints = check_unit_tests_hints_unif tests
   val _ = Lecker.test_group ctxt () [
       check_hints true [] "unify" closed_unify,
       check_hints true [] "unify_hints" unify_hints
     ]
 \<close>
 
 paragraph \<open>Unit Tests\<close>
 subparagraph \<open>With Unification Hints\<close>
 
 ML_command\<open>
   let
     val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
       |> Variable.declare_term @{term "f :: (nat \<Rightarrow> nat) \<times> nat \<Rightarrow> nat"}
       |> Variable.declare_term @{term "g :: nat \<times> nat \<Rightarrow> nat"}
       |> Variable.declare_term @{term "h :: nat"}
     val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
       "?x \<equiv> (0 :: nat) \<Longrightarrow> ?y \<equiv> ?z \<Longrightarrow> ?x + ?y \<equiv> ?z",
       "(?x :: ?'X) \<equiv> (?y :: ?'X) \<Longrightarrow> id ?x \<equiv> ?y",
       "(?x1 :: nat) \<equiv> ?x2 \<Longrightarrow> (?y1 :: nat) \<equiv> ?y2 \<Longrightarrow> ?x1 + ?y1 \<equiv> ?y2 + ?x2"
     ]
     val tests = map (apply2 (Syntax.read_term ctxt)) [
       ("\<lambda> x y. 0 + 1 :: nat", "\<lambda> x y. 1 :: nat"),
       ("\<lambda> x. 0 + 0 + x :: nat", "\<lambda> x. x :: nat"),
       ("\<lambda> x y. 0 + Suc ?x", "\<lambda> x y. Suc 2"),
       ("\<lambda> (x :: nat) (y :: nat). y + (0 + x)", "\<lambda> (x :: nat) (y :: nat). x + (0 + y)"),
       ("f (\<lambda> u. g (?x, h), h)", "id (f (\<lambda> u. ?y, 0 + h))")
    ]
     val check_hints = check_unit_tests_hints_unif tests
   in
     Lecker.test_group ctxt () [
       check_hints false [] "unify" closed_unify,
       check_hints false [] "unify_hints without hints" unify_hints,
       check_hints true hints "unify_hints with hints" unify_hints
     ]
   end
 \<close>
 
 end
diff --git a/thys/ML_Unification/Tests/tests_base.ML b/thys/ML_Unification/Tests/tests_base.ML
--- a/thys/ML_Unification/Tests/tests_base.ML
+++ b/thys/ML_Unification/Tests/tests_base.ML
@@ -1,192 +1,190 @@
 (*  Title:      ML_Unification/tests_base.ML
     Author:     Kevin Kappelmann
 
 Basic setup for ML unifier tests.
 
 TODO: generalise for unifiers with open terms; currently, all tests work with closed terms.
 *)
 signature UNIFICATION_TESTS_BASE =
 sig
 
   structure Hints : TERM_INDEX_UNIFICATION_HINTS
   val add_hint : Unification_Hints_Base.unif_hint -> Context.generic -> Context.generic
   val add_hints : thm list -> Proof.context -> Proof.context
 
   val term_gen : Proof.context -> int -> int -> int * int * int * int ->
     (int -> int -> int SpecCheck_Generator.gen) -> term SpecCheck_Generator.gen
   val term_pair_gen : Proof.context -> int -> int -> int * int * int * int ->
     (int -> int -> int SpecCheck_Generator.gen) ->
     (term * term) SpecCheck_Generator.gen
 
   val term_gen' : Proof.context -> int -> int -> int * int * int * int -> int ->
     int -> term SpecCheck_Generator.gen
   val term_pair_gen' : Proof.context -> int -> int -> int * int * int * int ->
     int -> int -> (term * term) SpecCheck_Generator.gen
 
   val thms_correct : (Envir.env -> (term * term) -> (term * term)) ->
     Envir_Normalisation.thm_normaliser -> Proof.context -> Unification_Base.closed_unifier ->
     (term * term) SpecCheck_Property.pred
 
   val terms_unify : Proof.context -> Unification_Base.closed_unifier ->
     (term * term) SpecCheck_Property.pred
 
   val terms_unify_thms_correct : (Envir.env -> (term * term) -> (term * term)) ->
     Envir_Normalisation.thm_normaliser -> Proof.context -> Unification_Base.closed_unifier ->
     (term * term) SpecCheck_Property.pred
 
   val terms_unify_thms_correct_unif : Proof.context -> Unification_Base.closed_unifier ->
     (term * term) SpecCheck_Property.pred
 
   val terms_unify_thms_correct_match : Proof.context -> Unification_Base.closed_unifier ->
     (term * term) SpecCheck_Property.pred
 
   val check : (term * term, 'a) SpecCheck_Generator.gen_state -> string ->
     (term * term) SpecCheck_Property.prop ->
     (Proof.context, 'a) Lecker.test_state
 
   val check_thm : (Envir.env -> (term * term) -> (term * term)) -> Envir_Normalisation.thm_normaliser ->
     (term * term, 'a) SpecCheck_Generator.gen_state -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
   val check_thm_unif : (term * term, 'a) SpecCheck_Generator.gen_state -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
   val check_thm_match : (term * term, 'a) SpecCheck_Generator.gen_state -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
   val check_list : (term * term) list -> string ->
     (term * term) SpecCheck_Property.prop -> Proof.context ->
     (term * term) Seq.seq
 
   val check_unit_tests_hints : (Envir.env -> (term * term) -> (term * term)) ->
     Envir_Normalisation.thm_normaliser -> (term * term) list -> bool -> thm list -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
   val check_unit_tests_hints_unif : (term * term) list -> bool -> thm list -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
   val check_unit_tests_hints_match : (term * term) list -> bool -> thm list -> string ->
     Unification_Base.closed_unifier -> (Proof.context, 'a) Lecker.test_state
 
 end
 
 structure Unification_Tests_Base : UNIFICATION_TESTS_BASE =
 struct
 
 structure Hints = Test_Unification_Hints
 
 val add_hint = Test_Unification_Hints.add_hint_prio o rpair Prio.MEDIUM
 fun add_hints thms ctxt = fold add_hint thms (Context.Proof ctxt) |> Context.proof_of
 
 structure Gen = SpecCheck_Generator
 structure UUtil = Unification_Util
+structure CUtil = Conversion_Util
 structure Norm = Envir_Normalisation
+structure TNorm = Term_Normalisation
 
 fun term_num_args_gen nv ni weights num_args_gen h i =
   Gen.zip (Gen.aterm' (Gen.nonneg nv) (Gen.nonneg ni) weights) (num_args_gen h i)
 
 fun term_gen ctxt nv ni weights num_args_gen =
   let val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
   in
     Gen.term_tree (term_num_args_gen nv ni weights num_args_gen)
     |> Gen.map (try (singleton (Variable.polymorphic ctxt') o Syntax.check_term ctxt'))
     |> Gen.filter is_some
     |> Gen.map the
   end
 
 fun term_pair_gen ctxt nv ni weights num_args_gen =
   let
     val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
     val term_gen = Gen.term_tree (term_num_args_gen nv ni weights num_args_gen)
   in
     Gen.zip term_gen term_gen
     |> Gen.map (fn (s, t) => try (Variable.polymorphic ctxt' o Syntax.check_terms ctxt') [s, t])
     |> Gen.filter is_some
     |> Gen.map (fn SOME [s, t] => (s, t))
   end
 
 fun num_args_gen max_h max_args h _ = if h > max_h then Gen.return 0 else Gen.nonneg max_args
 
 fun term_gen' ctxt nv ni weights max_h max_args =
   term_gen ctxt nv ni weights (num_args_gen max_h max_args)
 
 fun term_pair_gen' ctxt nv ni weights max_h max_args =
   term_pair_gen ctxt nv ni weights (num_args_gen max_h max_args)
 
 fun show_termpair ctxt =
   let val pretty_term = Syntax.pretty_term ctxt
   in SpecCheck_Show.zip pretty_term pretty_term end
 
 val shrink_termpair = SpecCheck_Shrink.product SpecCheck_Shrink.term SpecCheck_Shrink.none
 
 fun thms_correct norm_terms norm_thm ctxt unif tp =
   let
     val env_thmq = unif ctxt tp (UUtil.empty_envir tp)
     fun thm_correct (env, thm) =
       let
         val (t1, t2) = norm_terms env tp
         val thm' = norm_thm ctxt env thm
         val (lhs, rhs) = Thm.concl_of thm' |> Logic.dest_equals
       in List.all Envir.aeconv [(t1, lhs), (t2, rhs)] andalso Thm.no_prems thm' end
   in List.all thm_correct (Seq.list_of env_thmq) end
 
 fun terms_unify ctxt unif tp =
   UUtil.empty_envir tp
   |> unif ctxt tp
   |> General_Util.seq_is_empty
   |> not o fst
 
 fun terms_unify_thms_correct norm_terms norm_thm ctxt unif tp =
   terms_unify ctxt unif tp andalso thms_correct norm_terms norm_thm ctxt unif tp
 
+val beta_eta_short_norm_term_unif = UUtil.inst_norm_term Norm.norm_term_unif TNorm.beta_eta_short
+val inst_norm_beta_eta_short_unif = UUtil.inst_norm_thm
+  (#inst_unif_thm UUtil.beta_eta_short_norms_unif) (#conv UUtil.beta_eta_short_norms_unif)
+val beta_eta_short_norm_term_match = UUtil.inst_norm_term Norm.norm_term_match TNorm.beta_eta_short
+val inst_norm_beta_eta_short_match = UUtil.inst_norm_thm
+  (#inst_unif_thm UUtil.beta_eta_short_norms_match) (#conv UUtil.beta_eta_short_norms_match)
+
 val terms_unify_thms_correct_unif = terms_unify_thms_correct
-  (apply2 o Norm.beta_eta_short_norm_term_unif)
-  (Norm.beta_eta_short_norm_thm Norm.norm_type_unif Norm.beta_eta_short_norm_term_unif)
+  (apply2 o beta_eta_short_norm_term_unif) inst_norm_beta_eta_short_unif
 
 val terms_unify_thms_correct_match = terms_unify_thms_correct
-  (apfst o Norm.beta_norm_term_match)
-  (*types are already normalised by matcher*)
-  (Norm.beta_eta_short_norm_thm (K I) Norm.beta_norm_term_match)
+  (apfst o beta_eta_short_norm_term_match) inst_norm_beta_eta_short_match
 
 fun check gen name prop ctxt =
   SpecCheck.check_shrink (show_termpair ctxt) shrink_termpair
     gen name prop ctxt
 
 fun check_thm norm_terms norm_thm gen name unif ctxt = check gen ("Theorem correctness: " ^ name)
   (SpecCheck_Property.==> (terms_unify ctxt unif, thms_correct norm_terms norm_thm ctxt unif))
   ctxt
 
-fun check_thm_unif norm_terms = check_thm
-  (apply2 o Norm.beta_eta_short_norm_term_unif)
-  (Norm.beta_eta_short_norm_thm Norm.norm_type_unif Norm.beta_eta_short_norm_term_unif)
-  norm_terms
+fun check_thm_unif norm_terms = check_thm (apply2 o beta_eta_short_norm_term_unif)
+  inst_norm_beta_eta_short_unif norm_terms
 
-fun check_thm_match norm_terms = check_thm
-  (apfst o Norm.beta_norm_term_match)
-  (Norm.beta_eta_short_norm_thm (K I) Norm.beta_norm_term_match)
+fun check_thm_match norm_terms = check_thm (apfst o beta_eta_short_norm_term_match) inst_norm_beta_eta_short_match
   norm_terms
 
 fun check_list tests name prop ctxt =
   SpecCheck.check_list (show_termpair ctxt) tests name prop ctxt
 
 fun check_unit_tests_hints norm_terms norm_thm tests should_succeed hints name unif ctxt s =
   let val ctxt' = add_hints hints ctxt
   in
     check_list tests name
       (SpecCheck_Property.prop
         (fn tp => terms_unify_thms_correct norm_terms norm_thm ctxt' unif tp = should_succeed))
       ctxt'
     |> K s
   end
 
 fun check_unit_tests_hints_unif norm_terms = check_unit_tests_hints
-  (apply2 o Norm.beta_eta_short_norm_term_unif)
-  (Norm.beta_eta_short_norm_thm Norm.norm_type_unif Norm.beta_eta_short_norm_term_unif)
-  norm_terms
+  (apply2 o beta_eta_short_norm_term_unif) inst_norm_beta_eta_short_unif norm_terms
 
 fun check_unit_tests_hints_match norm_terms = check_unit_tests_hints
-  (apfst o Norm.beta_norm_term_match)
-  (Norm.beta_eta_short_norm_thm (K I) (K I))
-  norm_terms
+  (apfst o beta_eta_short_norm_term_match) inst_norm_beta_eta_short_match norm_terms
 
 end
diff --git a/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy b/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy
--- a/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy
+++ b/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy
@@ -1,98 +1,100 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>Unification Hints\<close>
 theory ML_Unification_Hints
   imports
     ML_Unification_Hints_Base
     ML_Unifiers
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Setup of unification hints.\<close>
 
 text \<open>We now set up two unifiers using unification hints. The first one allows for recursive
 applications of unification hints when unifying a hint's conclusion \<open>lhs \<equiv> rhs\<close> with a goal
 \<open>lhs' \<equiv> rhs'\<close>.
 The second disallows recursive applications of unification hints. Recursive applications have to be
 made explicit in the hint itself (cf. @{dir "../Examples"}).
 
 While the former can be convenient for local hint registrations and quick developments,
 it is advisable to use the second for global hints to avoid unexpected looping behaviour.\<close>
 
 ML\<open>
   @{functor_instance struct_name = Standard_Unification_Hints_Rec
     and functor_name = Term_Index_Unification_Hints
     and id = \<open>"rec"\<close>
     and more_args = \<open>
       structure TI = Discrimination_Tree
       val init_args = {
         concl_unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify,
         prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
           |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
         normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify,
         retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval
           TI.norm_term TI.unifiables),
         hint_preprocessor = SOME (K I)
       }\<close>}
 \<close>
 local_setup \<open>Standard_Unification_Hints_Rec.setup_attribute NONE\<close>
 
 text\<open>Standard unification hints using
 @{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify}
 when looking for hints are accessible via @{attribute rec_uhint}.
 
 \<^emph>\<open>Note:\<close> when we retrieve a potential unification hint with conclusion \<open>lhs \<equiv> rhs\<close> for a goal
 \<open>lhs' \<equiv> rhs'\<close>, we only consider those hints whose lhs potentially higher-order unifies with
 lhs' or rhs' \<^emph>\<open>without using hints\<close>. For otherwise, any hint \<open>lhs \<equiv> rhs\<close> applied to a goal
 \<open>rhs \<equiv> lhs\<close> leads to an immediate loop.\<close>
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Standard_Unification_Hints_Rec.try_hints
   |> Unification_Combinator.norm_unifier
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
   |> K)
   (Standard_Unification_Combine.metadata Standard_Unification_Hints_Rec.binding Prio.LOW)\<close>]]
 
 ML\<open>
   @{functor_instance struct_name = Standard_Unification_Hints
     and functor_name = Term_Index_Unification_Hints
     and id = \<open>""\<close>
     and more_args = \<open>
       structure TI = Discrimination_Tree
       val init_args = {
         concl_unifier = NONE,
         prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
           |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
         normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify,
         retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval
           TI.norm_term TI.unifiables),
         hint_preprocessor = SOME (K I)
       }\<close>}
 \<close>
 local_setup \<open>Standard_Unification_Hints.setup_attribute NONE\<close>
 declare [[uhint where concl_unifier = \<open>fn binders =>
   Standard_Unification_Combine.delete_eunif_data
     (Standard_Unification_Combine.metadata Standard_Unification_Hints.binding (Prio.LOW + 1))
   (*TODO: should we also remove the recursive hint unifier here? time will tell...*)
   (*#> Standard_Unification_Combine.delete_eunif_data
     (Standard_Unification_Combine.metadata Standard_Unification_Hints_Rec.binding Prio.LOW)*)
   |> Context.proof_map
   #> Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify binders\<close>]]
 
 text\<open>Standard unification hints using
 @{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify} when looking for hints,
 without using fallback list of unifiers, are accessible via @{attribute uhint}.
 
 \<^emph>\<open>Note:\<close> there will be no recursive usage of unification hints when searching for potential
 unification hints in this case. See also @{dir "../Examples"}.\<close>
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Standard_Unification_Hints.try_hints
   |> Unification_Combinator.norm_unifier
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
   |> K)
   (Standard_Unification_Combine.metadata Standard_Unification_Hints.binding (Prio.LOW + 1))\<close>]]
 
 
 text\<open>Examples see @{dir "../Examples"}.\<close>
 
 end
diff --git a/thys/ML_Unification/Unification_Hints/unification_hints_base.ML b/thys/ML_Unification/Unification_Hints/unification_hints_base.ML
--- a/thys/ML_Unification/Unification_Hints/unification_hints_base.ML
+++ b/thys/ML_Unification/Unification_Hints/unification_hints_base.ML
@@ -1,145 +1,147 @@
 (*  Title:      ML_Unification/unification_hints_base.ML
     Author:     Kevin Kappelmann, Paul Bachmann
 
 Unification hints (introduced in "Hints in unification" by Asperti et al, 2009).
 We support a generalisation that
 1. allows additional universal variables in premises
 2. allows non-atomic left-hand sides for premises
 3. allows arbitrary functions to perform the matching/unification of a hint with
    a disagreement pair.
 
 General shape of a hint:
 \<open>\<And>y1...yn. (\<And>x1...xn1. lhs1 \<equiv> rhs1) \<Longrightarrow> ... \<Longrightarrow> (\<And>x1...xnk. lhsk \<equiv> rhsk) \<Longrightarrow> lhs \<equiv> rhs\<close>
 *)
 signature UNIFICATION_HINTS_BASE =
 sig
   include HAS_LOGGER
 
   type unif_hint = thm
   val cdest_hint : unif_hint -> (cterm * cterm) list * (cterm * cterm)
   val cdest_hint_concl : unif_hint -> cterm * cterm
   val symmetric_hint : unif_hint -> unif_hint
   val pretty_hint : Proof.context -> unif_hint -> Pretty.T
 
   type hint_preprocessor = Proof.context -> thm -> unif_hint
   val obj_logic_hint_preprocessor : thm -> conv -> hint_preprocessor
 
   val try_hint : Unification_Base.matcher -> Unification_Base.normalisers -> unif_hint ->
     Unification_Base.e_unifier
 
   type hint_retrieval = term Binders.binders -> Proof.context -> term * term -> Envir.env ->
     unif_hint Seq.seq
 
   val try_hints : hint_retrieval -> Unification_Base.matcher -> Unification_Base.normalisers ->
     Unification_Base.e_unifier
 end
 
 structure Unification_Hints_Base : UNIFICATION_HINTS_BASE =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Unification_Hints_Base"
 
 structure GUtil = General_Util
 structure TUtil = Term_Util
 structure CUtil = Conversion_Util
 
 type unif_hint = thm
 
 val cdest_hint = Thm.cprop_of #> TUtil.strip_cimp #>> map Thm.dest_equals ##> Thm.dest_equals
 val cdest_hint_concl = Thm.cconcl_of #> Thm.dest_equals
 
 (*only flips the conclusion since unification calls for the premises should be symmetric*)
-val symmetric_hint = Conv.concl_conv ~1 CUtil.symmetric_conv |> CUtil.thm_conv
+val symmetric_hint = Conv.concl_conv ~1 CUtil.symmetric_conv |> CUtil.apply_thm_conv
 val pretty_hint = Thm.pretty_thm
 
 type hint_preprocessor = Proof.context -> thm -> unif_hint
 fun obj_logic_hint_preprocessor eq_eq_meta_eq default_conv ctxt =
   let
     fun eq_conv ct = (if can Thm.dest_equals ct then Conv.all_conv
       else Conv.rewr_conv eq_eq_meta_eq else_conv default_conv) ct
     val forall_eq_conv = Conversion_Util.repeat_forall_conv (K o K eq_conv)
-  in Conversion_Util.imp_conv (forall_eq_conv ctxt) eq_conv |> Conversion_Util.thm_conv end
+  in Conversion_Util.imp_conv (forall_eq_conv ctxt) eq_conv |> Conversion_Util.apply_thm_conv end
 
 (*Tries to apply a hint to solve E-unification of (t1 \<equiv>? t2).
 Vars in hint are lifted wrt. the passed binders.
 Unifies the hint's conclusion with (t1, t2) using match.
 Unifies resulting unification problems using unify.
 Normalises the terms and theorems after unify with norms.
 Returns a sequence of (env, thm) pairs.*)
 fun try_hint match norms hint unify binders ctxt (t1, t2)
   (Envir.Envir {maxidx, tenv, tyenv}) =
   let
     val dest_all_equals = TUtil.strip_all ##> Logic.dest_equals
     val rev_binders = rev binders
     val _ = @{log Logger.TRACE} ctxt (fn _ => Pretty.block [
         Pretty.str "Trying hint: ", pretty_hint ctxt hint
       ] |> Pretty.string_of)
     (*lift hint to include bound variables and increase indexes*)
     val lifted_hint =
       (*"P" is just some dummy proposition variable with appropriate index*)
       Logic.list_all (map fst rev_binders, Var (("P", maxidx + 1), propT))
       |> Thm.cterm_of ctxt
       (*lift bound variables to the hint*)
       |> GUtil.flip Thm.lift_rule hint
     val (hint_prems, hint_concl) = Thm.prop_of lifted_hint |> TUtil.strip_subgoal |> snd
 
     (*match hint with unification pair*)
     val (P, Q) = dest_all_equals hint_concl |> snd
     val match = match binders ctxt
     val (no_hint_match, match_env_concl_thmpq) =
       Envir.Envir {maxidx = Thm.maxidx_of lifted_hint, tenv = tenv, tyenv = tyenv}
       |> match (P, t1)
       |> Seq.maps (fn (env, thm1) => match (Q, t2) env |> Seq.map (apsnd (pair thm1)))
       |> GUtil.seq_is_empty
   in
     if no_hint_match then (@{log Logger.TRACE} ctxt (K "Hint does not match."); Seq.empty)
     else
       let
         val _ = @{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
             Pretty.str "Hint ",
             pretty_hint ctxt hint,
             Pretty.str ((length hint_prems > 0 ? suffix " Unifying premises...") " matched.")
           ] |> Pretty.string_of)
         (*unify each hint premise and collect the theorems while iteratively extending the environment*)
         fun unif_prem prem =
           let
             val (params, PQ_prem) = dest_all_equals prem
             val (binders, ctxt) = Binders.fix_binders params ctxt
             fun unif_add_result (env, thms) = unify binders ctxt PQ_prem env
               |> Seq.map (apsnd (fn thm => (binders, thm) :: thms))
           in Seq.maps unif_add_result end
         fun unify_prems (match_env, concl_thmp) =
           fold unif_prem hint_prems (Seq.single (match_env, []))
           |> Seq.map (rpair concl_thmp)
         fun inst_discharge ((env_res, prem_thms), concl_thmp) =
           let
             (*instantiate the theorems*)
-            val lifted_hint_inst = #norm_thm norms ctxt env_res lifted_hint
-            val norm_term = #norm_term norms env_res
-            val mk_norm_cbinders = map (Thm.cterm_of ctxt o norm_term o snd)
-            val norm_unif_thm = #norm_unif_thm norms ctxt env_res
-            fun forall_intr binders = fold Thm.forall_intr (mk_norm_cbinders binders) o norm_unif_thm
+            val conv = #conv norms
+            val lifted_hint_inst = Unification_Util.inst_norm_thm (#inst_thm norms) conv ctxt
+              env_res lifted_hint
+            val inst_term = #inst_term norms env_res
+            val mk_inst_cbinders = map (Thm.cterm_of ctxt o inst_term o snd)
+            val norm_unif_thm = Unification_Util.inst_norm_thm (#inst_unif_thm norms) conv ctxt env_res
+            fun forall_intr binders = fold Thm.forall_intr (mk_inst_cbinders binders) o norm_unif_thm
             val prem_thms_inst = map (uncurry forall_intr) prem_thms |> rev
             val (concl_thmL, concl_thmR) = apply2 norm_unif_thm concl_thmp
             (*discharge the hint premises*)
             val thm_res = Drule.implies_elim_list lifted_hint_inst prem_thms_inst
-              |> Drule.forall_elim_list (mk_norm_cbinders rev_binders)
+              |> Drule.forall_elim_list (mk_inst_cbinders rev_binders)
               |> GUtil.flip Thm.transitive concl_thmR
               |> Thm.transitive (Unification_Base.symmetric concl_thmL)
           in (env_res, thm_res) end
       in Seq.maps unify_prems match_env_concl_thmpq |> Seq.map inst_discharge end
   end
 
 type hint_retrieval = term Binders.binders -> Proof.context -> term * term -> Envir.env ->
   unif_hint Seq.seq
 
 fun try_hints get_hints match norms unif binders ctxt (t1, t2) env =
   (@{log Logger.TRACE} ctxt (fn _ =>
     Pretty.block [
       Pretty.str "Trying unification hints for ",
       Unification_Util.pretty_unif_problem ctxt (t1, t2)
     ] |> Pretty.string_of);
   get_hints binders ctxt (t1, t2) env
   |> Seq.maps (fn hint => try_hint match norms hint unif binders ctxt (t1, t2) env))
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML b/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML
--- a/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML
+++ b/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML
@@ -1,96 +1,98 @@
 (*  Title:      ML_Unification/unify_assumption_base.ML
     Author:     Kevin Kappelmann
 
 Assumption tactic with adjustable unifier.
 *)
 signature UNIFY_ASSUMPTION_BASE =
 sig
   include HAS_LOGGER
 
   val unify_assumption_tac_index : Unification_Base.normalisers -> Unification_Base.unifier ->
     Proof.context -> int -> thm -> (int * thm) Seq.seq
   val unify_assumption_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     Proof.context -> int -> tactic
 end
 
 structure Unify_Assumption_Base : UNIFY_ASSUMPTION_BASE =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Unify_Assumption_Base"
 
 structure UBase = Unification_Base
 
 local
 (*returns unification result and updated state where the unified assumption is moved to the front*)
 fun unify_assumption unify ctxt i state =
   (let
     val strip_subgoal = Term_Util.strip_nth_subgoal i
     val (rparams, (prems, _)) = strip_subgoal state
     val nprems = length prems
   in
     if nprems < 1 then Seq.empty
     else
       let
         val (binders, unif_ctxt) = Binders.fix_binders rparams ctxt
         fun prepare_nth_prem n prem =
           let val (params, nprems_prem) = Term_Util.strip_all prem ||> Logic.count_prems
           in
             if nprems - n < nprems_prem then Seq.empty (*too many subpremises in given premise*)
             else
               let val nprems_new = nprems - nprems_prem
               in
                 (*protect conclusion*)
                 Tactic_Util.protect_tac nprems_new ctxt i state
                 (*move premise to the front*)
                 |> Seq.maps (rotate_tac (n - 1) i)
                 (*remove all other premises*)
                 |> Seq.maps (Tactic_Util.thin_tacs (2 upto nprems_new) i)
                 (*remove outermost parameters of premise*)
                 |> Seq.maps (REPEAT_DETERM_N (length params) (dresolve_tac ctxt [@{thm Pure.meta_spec}] i))
                 (*protect premise*)
                 |> Seq.maps (dmatch_tac ctxt [Drule.protectI] i)
               end
           end
         fun mk_result prem_index state =
           (*unified assumption must be the first premise in the passed state*)
           (let val (_, (prem :: _, concl)) = strip_subgoal state
           in
             unify binders unif_ctxt (prem, concl) (Envir.empty (Thm.maxidx_of state))
             |> Seq.map (pair (prem_index, binders) o rpair state)
           end)
           handle TERM _ => Seq.empty
         fun unify_prem (n, prem) = let val prem_index = n + 1
           in
             prepare_nth_prem prem_index prem
             |> Seq.maps (mk_result prem_index)
             |> Seq.append
           end
       in General_Util.fold_rev_index unify_prem prems Seq.empty end
   end)
   handle TERM _ => Seq.empty
 in
 
 fun unify_assumption_tac_index norms unify ctxt i state =
   let
     val _ = @{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "Trying proof by assumption for subgoal ",
         Pretty.str (Int.toString i),
         Pretty.str ": ",
         (Thm.prop_of state |> Logic.nth_prem o pair i |> Syntax.pretty_term ctxt)
         handle TERM _ => Pretty.str "<no subgoal for given index>"
       ] |> Pretty.string_of)
     fun rewrite_subgoal ((n, binders), (res, state)) =
       (*rewrite conclusion to match the premise*)
-      Tactic_Util.rewrite_subgoal_unif_concl (#norm_term norms) (#norm_thm norms)
-        (#norm_unif_thm norms) binders res ctxt i state
+      Tactic_Util.rewrite_subgoal_unif_concl (#inst_term norms)
+        (Unification_Util.inst_norm_subgoal (#inst_thm norms) (#conv norms))
+        (Unification_Util.inst_norm_thm (#inst_unif_thm norms) (#conv norms))
+        binders res ctxt i state
       (*unified premise is moved to the front; now close by equality assumption*)
       |> Seq.maps (DETERM (Tactic_Util.nth_eq_assume_tac 1 i))
       |> Seq.map (pair n)
   in unify_assumption unify ctxt i state |> Seq.maps rewrite_subgoal end
 
 fun unify_assumption_tac norms =
   Seq.map snd oooo unify_assumption_tac_index norms
 
 end
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy b/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy
--- a/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy
+++ b/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy
@@ -1,89 +1,98 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 subsection \<open>Resolution Tactics\<close>
 theory Unify_Resolve_Tactics
   imports
     Unify_Resolve_Tactics_Base
     ML_Unifiers
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>Setup of resolution tactics and examples.\<close>
 
 ML\<open>
   @{functor_instance struct_name = Standard_Unify_Resolve
     and functor_name = Unify_Resolve
     and id = \<open>""\<close>
     and more_args = \<open>val init_args = {
       normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify,
       unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify,
       mode = SOME (Unify_Resolve_Args.PM.key Unify_Resolve_Args.PM.any),
       chained = SOME (Unify_Resolve_Args.PCM.key Unify_Resolve_Args.PCM.resolve)
     }\<close>}
 \<close>
 local_setup \<open>Standard_Unify_Resolve.setup_attribute NONE\<close>
 local_setup \<open>Standard_Unify_Resolve.setup_method NONE\<close>
 
 paragraph \<open>Examples\<close>
 
 experiment
 begin
 
 lemma
   assumes h: "\<And>x. PROP D x \<Longrightarrow> PROP C x"
   shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
   apply (urule h) \<comment>\<open>the line below is equivalent\<close>
   (* apply (rule h) *)
   oops
 
 lemma
   assumes h: "PROP C x"
   shows "PROP C x"
   by (urule h where unifier = First_Order_Unification.unify) \<comment>\<open>the line below is equivalent\<close>
   (* using [[urule unifier = First_Order_Unification.unify]] by (urule h) *)
 
 lemma
   assumes h: "\<And>x. PROP A x \<Longrightarrow> PROP D x"
   shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
   \<comment>\<open>use (r,e,d,f) to specify the resolution mode (resolution, elim, dest, forward)\<close>
   apply (urule (d) h) \<comment>\<open>the line below is equivalent\<close>
   (* apply (drule h) *)
   oops
 
+lemma
+  assumes h1: "\<And>x. PROP A x \<Longrightarrow> PROP D x"
+  and h2: "\<And>x. PROP D x \<Longrightarrow> PROP E x"
+  shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
+  \<comment>\<open>use (rr,re,rd,rf) to use repetition; in particular: \<open>(urule (rr)) \<simeq> intro\<close>\<close>
+  apply (urule (rd) h1 h2)
+  oops
+
+
 text\<open>You can specify how chained facts should be used. By default, @{method urule} works like
 @{method rule}: it uses chained facts to resolve against the premises of the passed rules.\<close>
 
 lemma
   assumes h1: "\<And>x. (PROP F x \<Longrightarrow> PROP E x) \<Longrightarrow> PROP C x"
   and h2: "\<And>x. PROP F x \<Longrightarrow> PROP E x"
   shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
   \<comment>\<open>Compare all of the following calls:\<close>
   (* apply (rule h1) *)
   (* apply (urule h1) *)
   (* using h2 apply (rule h1) *)
   (* using h2 apply (urule h1) *)
   using h2 apply (urule h1 where chained = fact)
   (* using h2 apply (urule h1 where chained = insert) *)
   done
 
 text\<open>You can specify whether any or every rule must resolve against the goal:\<close>
 
 lemma
   assumes h1: "\<And>x y. PROP C y \<Longrightarrow> PROP D x \<Longrightarrow> PROP C x"
   and h2: "\<And>x y. PROP C x \<Longrightarrow> PROP D x"
   and h3: "\<And>x y. PROP C x"
   shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
   using h3 apply (urule h1 h2 where mode = every)
   (* using h3 apply (urule h1 h2) *)
   done
 
 lemma
   assumes h1: "\<And>x y. PROP C y \<Longrightarrow> PROP A x \<Longrightarrow> PROP C x"
   and h2: "\<And>x y. PROP C x \<Longrightarrow> PROP B x \<Longrightarrow> PROP D x"
   and h3: "\<And>x y. PROP C x"
   shows "\<And>x. PROP A x \<Longrightarrow> PROP B x \<Longrightarrow> PROP C x"
   using h3 apply (urule (d) h1 h2 where mode = every)
   oops
 
 end
 
 end
diff --git a/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML
--- a/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML
+++ b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML
@@ -1,277 +1,285 @@
 (*  Title:      ML_Unification/unify_resolve.ML
     Author:     Kevin Kappelmann
 
 Unification-resolution tactics with arguments from context.
 *)
 @{parse_entries (sig) PARSE_UNIFY_RESOLVE_ARGS
   [normalisers, unifier, mode, chained, resolve_mode, rules]}
 
 @{parse_entries (sig) PARSE_UNIFY_RESOLVE_CONTEXT_ARGS
   [normalisers, unifier, mode, chained]}
 
 @{parse_entries (sig) PARSE_UNIFY_RESOLVE_MODES [any, every]}
 
 @{parse_entries (sig) PARSE_UNIFY_RESOLVE_CHAINED_MODES [insert, resolve, fact]}
 
-@{parse_entries (sig) PARSE_UNIFY_RESOLVE_RESOLVE_MODES [r, e, d, f]}
+@{parse_entries (sig) PARSE_UNIFY_RESOLVE_RESOLVE_MODES [r, rr, e, re, d, rd, f, rf]}
 
 signature UNIFY_RESOLVE_ARGS =
 sig
   include HAS_LOGGER
 
   structure PA : PARSE_UNIFY_RESOLVE_ARGS
   structure PCA : PARSE_UNIFY_RESOLVE_CONTEXT_ARGS
 
   val PCA_entries_from_PA_entries : ('a, 'b, 'c, 'd, 'e, 'f) PA.entries -> ('a, 'b, 'c, 'd) PCA.entries
   val PA_entries_from_PCA_entries : ('a, 'b, 'c, 'd) PCA.entries -> 'e -> 'f ->
     ('a, 'b, 'c, 'd, 'e, 'f) PA.entries
 
   structure PM : PARSE_UNIFY_RESOLVE_MODES
   type mode = PM.key
   val parse_mode : mode parser
 
   structure PCM : PARSE_UNIFY_RESOLVE_CHAINED_MODES
   type chained_mode = PCM.key
   val parse_chained_mode : chained_mode parser
 
   structure PRM : PARSE_UNIFY_RESOLVE_RESOLVE_MODES
   type resolve_mode = PRM.key
   val parse_resolve_mode : resolve_mode parser
 
   type args = (Unification_Base.normalisers, Unification_Base.unifier, mode, chained_mode,
     resolve_mode, thm list) PA.entries
   type context_args = (Unification_Base.normalisers, Unification_Base.unifier, mode,
     chained_mode) PCA.entries
 
   val unify_resolve_tac : args -> thm list -> Proof.context -> int -> tactic
   val unify_resolve_context_args_tac : context_args -> resolve_mode -> thm list -> thm list ->
     Proof.context -> int -> tactic
 
   val arg_parsers : (ML_Code_Util.code parser, ML_Code_Util.code parser, mode parser,
     chained_mode parser, resolve_mode parser, thm list context_parser) PA.entries
 end
 
 structure Unify_Resolve_Args : UNIFY_RESOLVE_ARGS =
 struct
 
 structure URB = Unify_Resolve_Base
 
 val logger = Logger.setup_new_logger URB.logger "Unify_Resolve_Args"
 
 @{parse_entries (struct) PA
   [normalisers, unifier, mode, chained, resolve_mode, rules]}
 @{parse_entries (struct) PCA
   [normalisers, unifier, mode, chained]}
 
 fun PCA_entries_from_PA_entries {normalisers = normalisers, unifier = unifier, mode = mode,
   chained = chained,...} =
   {normalisers = normalisers, unifier = unifier, mode = mode, chained = chained}
 fun PA_entries_from_PCA_entries {normalisers = normalisers, unifier = unifier, mode = mode,
   chained = chained} resolve__mode rules = {normalisers = normalisers, unifier = unifier,
   mode = mode, chained = chained, resolve_mode = SOME resolve__mode, rules = SOME rules}
 
 @{parse_entries (struct) PM [any, every]}
 type mode = PM.key
 val parse_mode = PM.parse_key
 
 @{parse_entries (struct) PCM [insert, resolve, fact]}
 type chained_mode = PCM.key
 val parse_chained_mode = PCM.parse_key
 
-@{parse_entries (struct) PRM [r, e, d, f]}
+@{parse_entries (struct) PRM [r, rr, e, re, d, rd, f, rf]}
 type resolve_mode = PRM.key
 val parse_resolve_mode = PRM.parse_key
 
 type args = (Unification_Base.normalisers, Unification_Base.unifier, mode, chained_mode,
   resolve_mode, thm list) PA.entries
 type context_args = (Unification_Base.normalisers, Unification_Base.unifier, mode,
   chained_mode) PCA.entries
 
 fun unify_resolve_tac args chained_facts ctxt i =
   let
     val norms = PA.get_normalisers args
     val unify = PA.get_unifier args
     val mode = PA.get_mode args
-    val resolve_fn = (case (PA.get_resolve_mode args, mode) of
+    fun rmode_repeat rmode = case rmode of
+        PRM.rr _ => (PRM.key PRM.r, true)
+      | PRM.re _ => (PRM.key PRM.e, true)
+      | PRM.rd _ => (PRM.key PRM.d, true)
+      | PRM.rf _ => (PRM.key PRM.f, true)
+      | _ => (rmode, false)
+    val (rmode, repeat) = rmode_repeat (PA.get_resolve_mode args)
+    val resolve_fn = (case (rmode, mode) of
         (PRM.r _, PM.any _) => URB.unify_resolve_any_tac
       | (PRM.r _, PM.every _) => URB.unify_resolve_every_tac
         (*note: for e-resolution, we use the passed unifier to unify the conclusion
           as well as the premise of the elim-rule*)
       | (PRM.e _, PM.any _) => URB.unify_eresolve_any_tac norms unify
       | (PRM.e _, PM.every _) => URB.unify_eresolve_every_tac norms unify
       | (PRM.d _, PM.any _) => URB.unify_dresolve_any_tac
       | (PRM.d _, PM.every _) => URB.unify_dresolve_every_tac
       | (PRM.f _, PM.any _) => URB.unify_fresolve_any_tac
       | (PRM.f _, PM.every _) => URB.unify_fresolve_every_tac)
         norms unify
+      |> repeat ? (fn resolve_fn => CHANGED_PROP oo REPEAT_ALL_NEW oo resolve_fn)
     val rules = PA.get_rules args
   in case PA.get_chained args of
       PCM.insert _ => (*insert chained facts*)
         (Tactic_Util.insert_tac chained_facts ctxt
         THEN' resolve_fn rules ctxt) i
     | cm => (*pre-process rules with chained facts*)
         let
           val process_rule_tac = (case cm of
               PCM.resolve _ => Unify_Resolve_Base.unify_resolve_every_tac
             | PCM.fact _ => Unify_Resolve_Base.unify_resolve_atomic_every_tac)
                 norms unify chained_facts ctxt
             |> HEADGOAL
           fun add_rulesq (is_empty, rulesq) = case (is_empty, mode) of
               (true, PM.any _) => I
             | (true, PM.every _) => Seq.fail
             | _ => Seq.maps (fn rules => Seq.map (fn rule => rule :: rules) rulesq)
           fun process_rule rule = process_rule_tac rule
             |> General_Util.seq_is_empty
             |> tap (fn (true, _) => @{log Logger.WARN} ctxt (fn _ => Pretty.block [
                   Pretty.str "Could not use chained facts for rule ",
                   Thm.pretty_thm ctxt rule
                 ] |> Pretty.string_of)
               | _ => ())
             |> add_rulesq
         in
           fold_rev process_rule rules (Seq.single [])
           |> Seq.lifts (fn rules => resolve_fn rules ctxt i)
         end
   end
 
 val unify_resolve_context_args_tac = unify_resolve_tac ooo PA_entries_from_PCA_entries
 
 val arg_parsers = {
   normalisers = SOME Unification_Parser.parse_normalisers,
   unifier = SOME Unification_Parser.parse_unifier,
   mode = SOME parse_mode,
   chained = SOME parse_chained_mode,
   resolve_mode = SOME parse_resolve_mode,
   rules = SOME (Parse_Util.nonempty_thms (K "must provide at least one rule to resolve"))
 }
 
 end
 
 signature UNIFY_RESOLVE =
 sig
   structure Data : GENERIC_DATA
 
   val get_args : Context.generic -> Unify_Resolve_Args.context_args
   val map_args : (Unify_Resolve_Args.context_args -> Unify_Resolve_Args.context_args) ->
     Context.generic -> Context.generic
 
   val get_normalisers : Context.generic -> Unification_Base.normalisers
   val map_normalisers : (Unification_Base.normalisers -> Unification_Base.normalisers) ->
     Context.generic -> Context.generic
 
   val get_unifier : Context.generic -> Unification_Base.unifier
   val map_unifier : (Unification_Base.unifier -> Unification_Base.unifier) ->
     Context.generic -> Context.generic
 
   val get_mode : Context.generic -> Unify_Resolve_Args.mode
   val map_mode : (Unify_Resolve_Args.mode -> Unify_Resolve_Args.mode) ->
     Context.generic -> Context.generic
 
   val get_chained : Context.generic -> Unify_Resolve_Args.chained_mode
   val map_chained : (Unify_Resolve_Args.chained_mode -> Unify_Resolve_Args.chained_mode) ->
     Context.generic -> Context.generic
 
   val unify_resolve_tac : Unify_Resolve_Args.resolve_mode -> thm list -> thm list -> Proof.context ->
     int -> tactic
 
   val binding : binding
 
   val attribute : (ML_Code_Util.code, ML_Code_Util.code, Unify_Resolve_Args.mode,
     Unify_Resolve_Args.chained_mode) Unify_Resolve_Args.PCA.entries * Position.T -> attribute
   val parse_attribute : attribute parser
   val setup_attribute : string option -> local_theory -> local_theory
 
   val parse_method : (Proof.context -> Method.method) context_parser
   val setup_method : string option -> local_theory -> local_theory
 end
 
 functor Unify_Resolve(A : sig
     structure FIA : FUNCTOR_INSTANCE_ARGS
     val init_args : Unify_Resolve_Args.context_args
   end) : UNIFY_RESOLVE =
 struct
 
 structure URA = Unify_Resolve_Args
 structure PCA = URA.PCA
 structure PA = URA.PA
 structure PRM = URA.PRM
 structure FIU = Functor_Instance_Util(A.FIA)
 structure MCU = ML_Code_Util
 
 structure Data = Generic_Data(struct
   type T = URA.context_args
   val empty = A.init_args
   val merge = fst
 end)
 
 val get_args = Data.get
 val map_args = Data.map
 
 val get_normalisers = PCA.get_normalisers o get_args
 val map_normalisers = map_args o PCA.map_normalisers
 
 val get_unifier = PCA.get_unifier o get_args
 val map_unifier = map_args o PCA.map_unifier
 
 val get_mode = PCA.get_mode o get_args
 val map_mode = map_args o PCA.map_mode
 
 val get_chained = PCA.get_chained o get_args
 val map_chained = map_args o PCA.map_chained
 
 fun unify_resolve_tac resolve_mode rules facts ctxt =
   URA.unify_resolve_context_args_tac (get_args (Context.Proof ctxt)) resolve_mode rules facts
     ctxt
 
 val binding = FIU.mk_binding_id_prefix "urule"
 
 val parse_arg_entries =
   let
     val parsers = URA.arg_parsers |> URA.PCA_entries_from_PA_entries
     val parse_value = PCA.parse_entry (PCA.get_normalisers parsers)
       (PCA.get_unifier parsers) (PCA.get_mode parsers) (PCA.get_chained parsers)
     val parse_entry = Parse_Key_Value.parse_entry PCA.parse_key Parse_Util.eq parse_value
   in PCA.parse_entries_required Parse.and_list1 [] parse_entry (PCA.empty_entries ()) end
 
 fun attribute (entries, pos) =
   let
     fun URA_substructure_op substructure operation =
       MCU.flat_read ["Unify_Resolve_Args.", substructure, ".", operation]
     val [code_PM_op, code_PCM_op, code_PCA_op] = map URA_substructure_op ["PM", "PCM", "PCA"]
     val code_from_key = code_PCA_op o PCA.key_to_string
     fun code_from_entry (PCA.normalisers c) = c
       | code_from_entry (PCA.unifier c) = c
       | code_from_entry (PCA.mode m) = code_PM_op "key" @ code_PM_op (URA.PM.key_to_string m)
       | code_from_entry (PCA.chained cm) = code_PCM_op "key" @ code_PCM_op (URA.PCM.key_to_string cm)
     val code_entries = PCA.key_entry_entries_from_entries entries
       |> map (fn (k, v) => code_from_key k @ MCU.atomic (code_from_entry v))
       |> MCU.list
     val code =
       FIU.code_struct_op "map_args" @ MCU.atomic (code_PCA_op "merge_entries" @
       MCU.atomic (code_PCA_op "entries_from_entry_list" @ code_entries))
   in ML_Attribute.run_map_context (code, pos) end
 
 val parse_attribute = (parse_arg_entries |> Parse_Util.position) >> attribute
 
 val setup_attribute = Attrib.local_setup binding
   (Parse.!!! parse_attribute |> Scan.lift) o
   the_default ("set unify-resolution arguments (" ^ FIU.FIA.full_name ^ ")")
 
 val parse_method =
   let val parse_resolve_mode = Scan.optional
     (Parse_Util.parenths (PA.get_resolve_mode URA.arg_parsers |> Parse.!!!))
     (PRM.key PRM.r)
   in
     Scan.lift parse_resolve_mode
     -- PA.get_rules URA.arg_parsers
     -- ((Parse.where_ |-- parse_attribute) |> Parse.!!! |> Parse_Util.option |> Scan.lift)
     >> (fn ((resolve_mode, rules), opt_attr) =>
       the_default I (Option.map ML_Attribute_Util.attribute_map_ctxt opt_attr)
       #> Method_Util.METHOD_CONTEXT' (unify_resolve_tac resolve_mode rules))
   end
 
 val setup_method = Method.local_setup binding parse_method o
   the_default ("r/e/d/f-resolve rule(s) with first subgoal; with adjustable unifier ("
     ^ FIU.FIA.full_name ^ ")")
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML
--- a/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML
+++ b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML
@@ -1,201 +1,204 @@
 (*  Title:      ML_Unification/unify_resolve_base.ML
     Author:     Kevin Kappelmann
 
 Resolution with adjustable unifier.
 *)
 signature UNIFY_RESOLVE_BASE =
 sig
   include HAS_LOGGER
 
   (*unify the conclusions of the rule and the subgoal and resolve*)
   val unify_resolve_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm -> Proof.context -> int -> tactic
   val unify_resolve_every_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic
   val unify_resolve_any_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic
   (*treats the rule and subgoal as atomic propositions; example:
     resolving rule A ==> B and subgoal A ==> B leads to A ==> A while
     resolving rule A ==> B and subgoal A ==> B atomically solves the subgoal*)
   val unify_resolve_atomic_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm -> Proof.context -> int -> tactic
   val unify_resolve_atomic_every_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic
   val unify_resolve_atomic_any_tac : Unification_Base.normalisers ->
     Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic
 
   val unify_eresolve_tac_index : Unification_Base.normalisers -> Unification_Base.unifier ->
     Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context ->
     int -> thm -> (int * thm) Seq.seq
   val unify_eresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     Unification_Base.normalisers -> Unification_Base.unifier -> thm ->
     Proof.context -> int -> tactic
   val unify_eresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     Unification_Base.normalisers -> Unification_Base.unifier -> thm list ->
     Proof.context -> int -> tactic
   val unify_eresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     Unification_Base.normalisers -> Unification_Base.unifier -> thm list ->
     Proof.context -> int -> tactic
 
   val unify_dresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm ->
     Proof.context -> int -> tactic
   val unify_dresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     thm list -> Proof.context -> int -> tactic
   val unify_dresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     thm list -> Proof.context -> int -> tactic
 
   val unify_fresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm ->
     Proof.context -> int -> tactic
   val unify_fresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     thm list -> Proof.context -> int -> tactic
   val unify_fresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier ->
     thm list -> Proof.context -> int -> tactic
 
 end
 
 structure Unify_Resolve_Base : UNIFY_RESOLVE_BASE =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Unify_Resolve_Base"
 
 structure Util = Unification_Util
 structure HOPU = Higher_Order_Pattern_Unification
 
 fun unify_resolve_tac norms unify rule ctxt =
   let fun tac cgoal i state =
     let
       val _ = @{log Logger.TRACE} ctxt (fn _ =>
           Pretty.block [
             Pretty.str ("Calling unification resolution tactic on subgoal "),
             Pretty.str (Int.toString i),
             Pretty.str ": ",
             Util.pretty_terms ctxt [Thm.term_of cgoal],
             Pretty.str (" and rule: "),
             Thm.pretty_thm ctxt rule
           ]
           |> Pretty.string_of
         )
       val lifted_rule = Thm.lift_rule cgoal (Drule.incr_indexes state rule)
       val nprems_rule = Thm.nprems_of rule
       val rparams = Term_Util.strip_all (Thm.term_of cgoal) |> fst
       val (binders, ctxt) = Binders.fix_binders rparams ctxt
       val conclp = (*only unify the conclusion of the rule and the goal*)
         apply2 Logic.strip_assums_concl (Thm.prop_of lifted_rule, Thm.term_of cgoal)
       val env_thmq = unify binders ctxt conclp (Envir.empty (Thm.maxidx_of lifted_rule))
-      val norm_thm = #norm_thm norms
+      val conv = #conv norms
+      val inst_thm = #inst_thm norms
       fun rewrite_tac (env, unif_thm) =
-        Tactic_Util.rewrite_subgoal_unif_concl (#norm_term norms) norm_thm (#norm_unif_thm norms)
+        Tactic_Util.rewrite_subgoal_unif_concl (#inst_term norms)
+          (Util.inst_norm_subgoal inst_thm conv) (Util.inst_norm_thm (#inst_unif_thm norms) conv)
           binders (env, unif_thm) ctxt
-        THEN' Tactic_Util.no_lift_resolve_tac (norm_thm ctxt env lifted_rule) nprems_rule ctxt
+        THEN' (fn i => Tactic_Util.no_lift_resolve_tac
+          (Util.inst_norm_thm inst_thm conv ctxt env lifted_rule) nprems_rule ctxt i)
     in Seq.maps (fn res => rewrite_tac res i state) env_thmq end
   in Tactic_Util.CSUBGOAL_DATA I tac end
 
 fun unify_resolve_tacs norms unify rules ctxt =
   map (fn rule => unify_resolve_tac norms unify rule ctxt) rules
 
 fun unify_resolve_every_tac norms unify rules =
   unify_resolve_tacs norms unify rules #> EVERY'
 
 fun unify_resolve_any_tac norms unify rules =
   unify_resolve_tacs norms unify rules #> Tactic_Util.CONCAT'
 
 fun unify_resolve_atomic_tac norms unify rule ctxt =
   Tactic_Util.protect_tac 0 ctxt
   THEN' unify_resolve_tac norms unify (Thm_Util.protect rule) ctxt
 
 fun unify_resolve_atomic_tacs norms unify rules ctxt =
   map (fn rule => unify_resolve_atomic_tac norms unify rule ctxt) rules
 
 fun unify_resolve_atomic_every_tac norms unify rules =
   unify_resolve_atomic_tacs norms unify rules #> EVERY'
 
 fun unify_resolve_atomic_any_tac norms unify rules =
   unify_resolve_atomic_tacs norms unify rules #> Tactic_Util.CONCAT'
 
 fun unify_eresolve_tac_index norms_resolve unify_resolve norms_assume unify_assume
   rule ctxt i state =
   unify_resolve_tac norms_resolve unify_resolve rule ctxt i state
   |> Seq.maps (Unify_Assumption_Base.unify_assumption_tac_index norms_assume unify_assume ctxt i)
 
 fun unify_eresolve_tac norms_resolve unify_resolve norms_assume unify_assume
   rule ctxt i state =
   let val nprems = Thm.nprems_of rule
   in
     if nprems = 0 then
       (@{log Logger.WARN} ctxt (fn _ =>
         Pretty.block [
           Pretty.str "elim-resolution rule ",
           Thm.pretty_thm ctxt rule,
           Pretty.str " has no premises."
         ] |> Pretty.string_of
       );
       Seq.empty)
     else
       unify_eresolve_tac_index norms_resolve unify_resolve norms_assume unify_assume rule ctxt i state
       |> Seq.maps (fn (n, state) =>
         Tactic_Util.EVERY_ARG (Tactic_Util.thin_tac n) (i upto i + nprems - 2) state)
   end
 
 fun unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules ctxt =
   map (fn rule => unify_eresolve_tac norms_resolve unify_resolve norms_assume unify_assume rule ctxt)
     rules
 
 fun unify_eresolve_every_tac norms_resolve unify_resolve norms_assume unify_assume rules =
   unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules
   #> EVERY'
 
 fun unify_eresolve_any_tac norms_resolve unify_resolve norms_assume unify_assume rules =
   unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules
   #> Tactic_Util.CONCAT'
 
 fun unify_dresolve_tac norms unify rule ctxt =
   let val nprems = Thm.nprems_of rule
   in
     if nprems = 0 then
       (@{log Logger.WARN} ctxt (fn _ =>
         Pretty.block [
           Pretty.str "destruct-resolution rule ",
           Thm.pretty_thm ctxt rule,
           Pretty.str " has no premises."
         ] |> Pretty.string_of
       );
       K no_tac)
     else unify_eresolve_tac HOPU.norms_unify HOPU.unify norms unify (Tactic.make_elim rule) ctxt
   end
 
 fun unify_dresolve_tacs norms unify rules ctxt =
   map (fn rule => unify_dresolve_tac norms unify rule ctxt) rules
 
 fun unify_dresolve_every_tac norms unify rules = unify_dresolve_tacs norms unify rules #> EVERY'
 
 fun unify_dresolve_any_tac norms unify rules =
   unify_dresolve_tacs norms unify rules #> Tactic_Util.CONCAT'
 
 fun unify_fresolve_tac norms unify rule ctxt i state =
   let val nprems = Thm.nprems_of rule
   in
     if nprems = 0 then
       (@{log Logger.WARN} ctxt (fn _ =>
         Pretty.block [
           Pretty.str "forward-resolution rule ",
           Thm.pretty_thm ctxt rule,
           Pretty.str " has no premises."
         ] |> Pretty.string_of
       );
       Seq.empty)
     else
       unify_eresolve_tac_index HOPU.norms_unify HOPU.unify norms unify (Tactic.make_elim rule)
         ctxt i state
       |> Seq.map snd
   end
 
 fun unify_fresolve_tacs norms unify rules ctxt =
   map (fn rule => unify_fresolve_tac norms unify rule ctxt) rules
 
 fun unify_fresolve_every_tac norms unify rules =
   unify_fresolve_tacs norms unify rules #> EVERY'
 
 fun unify_fresolve_any_tac norms unify rules =
   unify_fresolve_tacs norms unify rules #> Tactic_Util.CONCAT'
 
 end
diff --git a/thys/ML_Unification/Unifiers/ML_Unifiers.thy b/thys/ML_Unification/Unifiers/ML_Unifiers.thy
--- a/thys/ML_Unification/Unifiers/ML_Unifiers.thy
+++ b/thys/ML_Unification/Unifiers/ML_Unifiers.thy
@@ -1,69 +1,71 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 theory ML_Unifiers
   imports
     ML_Functor_Instances
     ML_Priorities
     ML_Unifiers_Base
     Simps_To
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>More unifiers.\<close>
 
 paragraph \<open>Derived Unifiers\<close>
 
 ML_file\<open>higher_order_pattern_decomp_unification.ML\<close>
 ML_file\<open>var_higher_order_pattern_unification.ML\<close>
 
 paragraph \<open>Unification via Tactics\<close>
 
 ML_file\<open>tactic_unification.ML\<close>
 
 subparagraph \<open>Unification via Simplification\<close>
 
 lemma eq_if_SIMPS_TO_UNIF_if_SIMPS_TO:
   assumes "PROP SIMPS_TO t t'"
   and "PROP SIMPS_TO_UNIF s t'"
   shows "s \<equiv> t"
   using assms by (simp add: SIMPS_TO_eq SIMPS_TO_UNIF_eq)
 
 ML_file\<open>simplifier_unification.ML\<close>
 
 paragraph \<open>Combining Unifiers\<close>
 
 ML_file\<open>unification_combine.ML\<close>
 ML\<open>
   @{functor_instance struct_name = Standard_Unification_Combine
     and functor_name = Unification_Combine
     and id = \<open>""\<close>}
 \<close>
 local_setup \<open>Standard_Unification_Combine.setup_attribute NONE\<close>
 
 paragraph \<open>Mixture of Unifiers\<close>
 
 ML_file\<open>mixed_unification.ML\<close>
 ML\<open>
   @{functor_instance struct_name = Standard_Mixed_Unification
     and functor_name = Mixed_Unification
     and id = \<open>""\<close>
     and more_args = \<open>structure UC = Standard_Unification_Combine\<close>}
 \<close>
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Var_Higher_Order_Pattern_Unification.e_unify Unification_Combinator.fail_unify
   |> Unification_Combinator.norm_unifier
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
   |> K)
   (Standard_Unification_Combine.metadata \<^binding>\<open>var_hop_unif\<close> Prio.HIGH)\<close>]]
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Simplifier_Unification.simp_unify_progress Envir.aeconv Simplifier_Unification.simp_unify
-    (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
+    (Unification_Util.inst_norm_term'
+      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
     Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify
     Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
   |> Type_Unification.e_unify Unification_Util.unify_types
   |> K)
   (Standard_Unification_Combine.default_metadata \<^binding>\<open>simp_unif\<close>)
   \<close>]]
 
 end
diff --git a/thys/ML_Unification/Unifiers/first_order_unification.ML b/thys/ML_Unification/Unifiers/first_order_unification.ML
--- a/thys/ML_Unification/Unifiers/first_order_unification.ML
+++ b/thys/ML_Unification/Unifiers/first_order_unification.ML
@@ -1,235 +1,235 @@
 (*  Title:      ML_Unification/first_order_unification.ML
     Author:     Kevin Kappelmann, Paul Bachmann
 
 First-order E-unification.
 *)
 signature FIRST_ORDER_UNIFICATION =
 sig
   include HAS_LOGGER
 
   (* e-matching *)
   val e_match : Unification_Base.type_matcher -> Unification_Base.e_matcher
   val match : Unification_Base.matcher
   val norms_match : Unification_Base.normalisers
 
   (* e-unification *)
   val e_unify : Unification_Base.type_unifier -> Unification_Base.e_unifier
   val unify : Unification_Base.unifier
   val norms_unify : Unification_Base.normalisers
 end
 
 structure First_Order_Unification : FIRST_ORDER_UNIFICATION =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "First_Order_Unification"
 
 (* shared utils *)
 structure Util = Unification_Util
 structure Norm = Envir_Normalisation
 
 exception FALLBACK
 
 (*check if sequence is empty or raise FALLBACK exception*)
 fun seq_try sq = General_Util.seq_try FALLBACK sq
 
 
 (* e-matching *)
 
 val norms_match = Util.eta_short_norms_match
 
 (*Note: by E-matching we mean "matching modulo equalities" in the general sense,
 i.e. when matching p \<equiv>? t, t may contain variables.*)
 fun e_match match_types match_theory binders ctxt pt env =
   let
-    val norm_pt = apfst o (#norm_term norms_match)
+    val norm_pt = apfst o Util.inst_norm_term' norms_match
     fun rigid_rigid ctxt p n env = (*normalise the types in rigid-rigid cases*)
       Util.rigid_rigid Norm.norm_term_types_match match_types ctxt p n env |> seq_try
       handle Unification_Base.UNIF => Seq.empty (*types do not match*)
     (*standard first-order matcher that calls match_theory on failure;
     generated theorem is already normalised wrt. the resulting environment*)
     fun match binders ctxt (pt as (p, t)) (env as Envir.Envir {tenv, tyenv,...}) =
       (case pt of
         (Var (x, Tx), _) =>
           (case Envir.lookup1 tenv (x, Norm.norm_type_match tyenv Tx) of
             NONE =>
               if Term.is_open t then
                 (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
                     Pretty.str "Failed to match (open term) ",
                     Util.pretty_unif_problem ctxt (norm_pt env pt)
                   ] |> Pretty.string_of);
                 (*directly return empty sequence because the theory unifier
                 cannot do anything meaningful at this point*)
                 raise FALLBACK)
               else
                 let val Tt = fastype_of1 (Binders.binder_types binders, t)
                 in
                   ((match_types ctxt (Tx, Tt) env, Unification_Base.reflexive_term ctxt t)
                   (*insert new substitution x \<mapsto> t*)
                   |>> Envir.update ((x, Tt), t)
                   |> Seq.single)
                   handle Unification_Base.UNIF => Seq.empty (*types do not match*)
                 end
           | SOME p' =>
             if Envir.aeconv (apply2 Envir.beta_norm (p', t)) then
               Seq.single (env, Unification_Base.reflexive_term ctxt t)
             else raise FALLBACK)
       | (Abs (np, Tp, tp), Abs (nt, Tt, tt)) =>
           ((let val name = if np = "" then nt else np
           in
             match_types ctxt (Tp, Tt) env
             |> Util.abstract_abstract (K I) match binders ctxt name Tt (tp, tt)
             |> seq_try
           end)
           handle Unification_Base.UNIF => Seq.empty) (*types do not match*)
       (*eta-expand on the fly*)
       | (Abs (np, Tp, tp), _) =>
           ((let val Ttarg = fastype_of1 (Binders.binder_types binders, t) |> Term.dest_funT |> fst
           in
             match_types ctxt (Tp, Ttarg) env
             |> Util.abstract_abstract (K I) match binders ctxt np Ttarg
                 (tp, incr_boundvars 1 t $ Bound 0)
             |> seq_try
           end)
           handle TYPE _ => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
               Pretty.str "First-order matching failed. Term is not of function type ",
               Util.pretty_unif_problem ctxt (norm_pt env pt)
             ]
             |> Pretty.string_of);
             Seq.empty)
           | Unification_Base.UNIF => Seq.empty) (*types do not match*)
       | (_, Abs (nt, Tt, tt)) =>
           ((let val Tp = Envir.fastype env (Binders.binder_types binders) p
           in
             match_types ctxt (Tp, fastype_of1 (Binders.binder_types binders, t)) env
             |> Util.abstract_abstract (K I) match binders ctxt nt Tt
                 (incr_boundvars 1 p $ Bound 0, tt)
             |> seq_try
           end)
           handle Unification_Base.UNIF => Seq.empty) (*types do not match*)
       | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env)
       | (Free _, Free g) => rigid_rigid ctxt p g env
       | (Const _, Const d) => rigid_rigid ctxt p d env
       | (f $ x, g $ y) =>
           (*Note: types of recursive theorems are already normalised ==> we have to
           pass the identity type normaliser*)
           Util.comb_comb (K o K I) (match binders) ctxt (f, x) (g, y) env |> seq_try
       | _ => raise FALLBACK)
       handle FALLBACK =>
         (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [
             Pretty.str "First-order matching failed.",
             Util.pretty_call_theory_match ctxt (norm_pt env pt)
           ] |> Pretty.block |> Pretty.string_of);
         match_theory binders ctxt pt env)
   in
     (@{log Logger.DEBUG} ctxt (fn _ =>
       Pretty.block [
         Pretty.str "First-order matching ",
         Util.pretty_unif_problem ctxt (norm_pt env pt)
       ] |> Pretty.string_of);
     match binders ctxt pt env)
   end
 
 (*standard first-order matching*)
 val match = e_match Util.match_types Unification_Combinator.fail_match
 
 (* e-unification *)
 
 (*occurs check*)
 fun occurs v (Var (x, _)) = x = v
   | occurs v (s $ t) = occurs v s orelse occurs v t
   | occurs v (Abs (_, _, t)) = occurs v t
   | occurs _ _ = false
 
 val norms_unify = Util.eta_short_norms_unif
 
 fun e_unify unify_types unify_theory binders ctxt st env =
   let
-    val norm_st = apply2 o (#norm_term norms_unify)
+    val norm_st = apply2 o Util.inst_norm_term' norms_unify
     fun rigid_rigid ctxt t n env = (*we do not have to normalise types in rigid-rigid cases*)
       Util.rigid_rigid (K I) unify_types ctxt t n env |> seq_try
       handle Unification_Base.UNIF => Seq.empty (*types do not unify*)
     (*standard first-order unifier that calls unify_theory on failure*)
     fun unif binders ctxt (st as (s, t)) env =
       (case st of
         (Var (x, Tx), _) =>
           let val unif' = unif binders ctxt
           in
             (unif' (Envir.norm_term_same env s, t) env
             handle Same.SAME =>
               (unif' (s, Envir.norm_term_same env t) env
               handle Same.SAME =>
                 if Term.is_open t then
                   (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
                       Pretty.str "Failed to unify (open term) ",
                       Util.pretty_unif_problem ctxt (norm_st env st)
                     ]
                     |> Pretty.string_of);
                   raise FALLBACK)
                 else
                   let
                     val vars_eq = is_Var t andalso x = fst (dest_Var t)
                     fun update_env env =
                       (*unifying x=x ==> no new term substitution necessary*)
                       if vars_eq then env
                       (*insert new substitution x \<mapsto> t*)
                       else Envir.vupdate ((x, Tx), t) env
                   in
                     if not vars_eq andalso occurs x t then
                       (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
                           Pretty.str "Failed to unify (occurs check) ",
                           Util.pretty_unif_problem ctxt (norm_st env st)
                         ] |> Pretty.string_of);
                       raise FALLBACK)
                     else
                       ((unify_types ctxt (Tx, Envir.fastype env (Binders.binder_types binders) t) env,
                         Unification_Base.reflexive_term ctxt s)
                       |>> update_env
                       |> Seq.single)
                       handle Unification_Base.UNIF => Seq.empty (*types do not unify*)
                   end))
           end
        | (_, Var _) => unif binders ctxt (t, s) env |> Seq.map (apsnd Unification_Base.symmetric)
        | (Abs (ns, Ts, ts), Abs (nt, Tt, tt)) =>
           ((let val name = if ns = "" then nt else ns
           in
             unify_types ctxt (Ts, Tt) env
             |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt name Ts (ts, tt)
             |> seq_try
           end)
           handle Unification_Base.UNIF => Seq.empty) (*types do not unify*)
       (*eta-expand on the fly*)
       | (Abs (ns, Ts, ts), _) =>
           ((let val Tp = apply2 (Envir.fastype env (Binders.binder_types binders)) (s, t)
           in
             unify_types ctxt Tp env
             |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt ns Ts
               (ts, incr_boundvars 1 t $ Bound 0)
             |> seq_try
           end)
           handle Unification_Base.UNIF => Seq.empty) (*types do not unify*)
       | (_, Abs _) => unif binders ctxt (t, s) env |> Seq.map (apsnd Unification_Base.symmetric)
       | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env)
       | (Free _, Free g) => rigid_rigid ctxt s g env
       | (Const _, Const d) => rigid_rigid ctxt s d env
       (*we have to normalise types in comb cases*)
       | (f $ x, g $ y) =>
           Util.comb_comb Norm.norm_thm_types_unif (unif binders) ctxt (f, x) (g, y) env |> seq_try
       | _ => raise FALLBACK)
       handle FALLBACK =>
         (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [
             Pretty.str "First-order unification failed.",
             Util.pretty_call_theory_unif ctxt (norm_st env st)
           ] |> Pretty.block |> Pretty.string_of);
         unify_theory binders ctxt st env)
   in
     (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "First-order unifying ",
         Util.pretty_unif_problem ctxt (norm_st env st)
       ] |> Pretty.string_of);
     unif binders ctxt st env)
   end
 
 (*standard first-order unification*)
 val unify = e_unify Util.unify_types Unification_Combinator.fail_unify
 
 end
diff --git a/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML b/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML
--- a/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML
+++ b/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML
@@ -1,474 +1,473 @@
 (*  Title:      ML_Unification/higher_order_pattern_unification.ML
     Author:     Tobias Nipkow, Christine Heinzelmann, Stefan Berghofer, and
                 Kevin Kappelmann TU Muenchen
 
 Higher-Order Patterns due to Tobias Nipkow.
 E-Unification and theorem construction due to Kevin Kappelmann.
 
 See also:
 Tobias Nipkow. Functional Unification of Higher-Order Patterns.
 In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993.
 
 TODO: optimize red by special-casing it
 *)
 signature HIGHER_ORDER_PATTERN_UNIFICATION =
 sig
   include HAS_LOGGER
 
   (* e-matching *)
   (*precondition: types of terms are matched*)
   val e_match : Unification_Base.type_matcher -> Unification_Base.matcher ->
     Unification_Base.e_matcher
   val match : Unification_Base.matcher
   val norms_match : Unification_Base.normalisers
 
   (* e-unification *)
   (*precondition: types of terms are unified*)
   val e_unify : Unification_Base.type_unifier -> Unification_Base.unifier ->
     Unification_Base.e_unifier
   val unify : Unification_Base.unifier
   val norms_unify : Unification_Base.normalisers
 end
 
 structure Higher_Order_Pattern_Unification : HIGHER_ORDER_PATTERN_UNIFICATION =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Higher_Order_Pattern_Unification"
 
 (* shared utils *)
 structure Util = Unification_Util
 structure Norm = Envir_Normalisation
 
 exception FALLBACK
 
 (*check if sequence is empty or raise FALLBACK exception*)
 fun seq_try sq = General_Util.seq_try FALLBACK sq
 
 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
 fun downto0 ([], n) = n = ~1
   | downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
 
 fun mkabs (binders, is, t) =
   let fun abstract i acc =
     let val ((x, T), _) = nth binders i
     in Abs (x, T, acc) end
   in fold_rev abstract is t end
 
 exception IDX
 
 fun idx [] _ = raise IDX
   | idx (i :: is) j = if i = j then length is else idx is j
 
 fun ints_of bs =
   (*collects arguments and checks if they are all distinct, bound variables*)
   let fun dest_check (Bound i) acc =
           if member (op =) acc i then raise Unification_Base.PATTERN else i :: acc
         | dest_check _ _ = raise Unification_Base.PATTERN
   in fold_rev dest_check bs [] end
 
 fun app (s, []) = s
   | app (s, (i :: is)) = app (s $ Bound i, is)
 
 (* matching *)
 
 fun mapbnd f =
   let fun mpb d (Bound i) = if i < d then Bound i else Bound (f (i - d) + d)
         | mpb d (Abs (s, T, t)) = Abs (s, T, mpb (d + 1) t)
         | mpb d (u1 $ u2) = (mpb d u1) $ (mpb d u2)
         | mpb _ atom = atom
   in mpb 0 end
 
 fun red (Abs (_, _, s)) (i :: is) js = red s is (i :: js)
   | red t [] [] = t
   | red t is jn = app (mapbnd (nth jn) t, is)
 
 exception OPEN_TERM
 
 fun match_bind (tenv, binders, ixn, T, is, t) =
   let val js = loose_bnos t
   in
     if null is then
       if null js then Vartab.update_new (ixn, (T, t)) tenv
       else raise OPEN_TERM
     else if subset (op =) (js, is) then
       let val t' = if downto0 (is, length binders - 1) then t else mapbnd (idx is) t
       in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) tenv end
     else raise OPEN_TERM
   end
 
 
 (** higher-order pattern E-unification **)
 val norms_match = Util.beta_eta_short_norms_match
 
 fun e_match match_types match_theory_pattern match_theory_fail binders ctxt pt env =
   let
-    val norm_pt = apfst o (#norm_term norms_match)
+    val norm_pt = apfst o Util.inst_norm_term' norms_match
     fun rigid_rigid ctxt p n env = (*normalise the types in rigid-rigid cases*)
       Util.rigid_rigid Norm.norm_term_types_match match_types ctxt p n env |> seq_try
       handle Unification_Base.UNIF => Seq.empty (*types do not match*)
     (*generated theorem is already normalised wrt. the resulting environment*)
     fun match binders ctxt (pt as (p, t)) (env as Envir.Envir {maxidx, tenv, tyenv}) =
       let
         (*call match_theory on failure*)
         fun handle_failure match_theory failure_msg =
           (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [
               failure_msg (),
               Util.pretty_call_theory_match ctxt (norm_pt env pt)
             ] |> Pretty.block |> Pretty.string_of);
           match_theory binders ctxt pt env)
       in
         (case pt of
           (Abs (np, _, tp), Abs (nt, Tt, tt)) =>
             let val name = if np = "" then nt else np
             in
               Util.abstract_abstract (K I) match binders ctxt name Tt (tp, tt) env
               |> seq_try
             end
         (*eta-expand on the fly*)
         | (Abs (np, Tp, tp), _) =>
             let val Tp' = Envir.subst_type tyenv Tp
             in
               Util.abstract_abstract (K I) match binders ctxt np Tp'
                 (tp, incr_boundvars 1 t $ Bound 0) env
               |> seq_try
             end
         | (_, Abs (nt, Tt, tt)) =>
             Util.abstract_abstract (K I) match binders ctxt nt Tt
               (incr_boundvars 1 p $ Bound 0, tt) env
             |> seq_try
         | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env)
         | (Free _, Free g) => rigid_rigid ctxt p g env
         | (Const _, Const d) => rigid_rigid ctxt p d env
         | _ => case strip_comb p of
             (Var (x, T), ps) =>
               let
                 val is = ints_of ps
                 val T' = Norm.norm_type_match tyenv T
               in
                 case Envir.lookup1 tenv (x, T') of
                   NONE =>
                     ((let
                       val tenv' = match_bind (tenv, binders, x, T', is, t)
                       val env' = Envir.Envir {maxidx=maxidx, tenv=tenv', tyenv=tyenv}
                       val t' = Binders.replace_binders binders t
                     in Seq.single (env', Unification_Base.reflexive_term ctxt t') end)
                     handle OPEN_TERM => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
                         Pretty.str "Failed to unify (open term) ",
                         Util.pretty_unif_problem ctxt (norm_pt env pt)
                       ] |> Pretty.string_of);
                       Seq.empty))
                 | SOME ph' =>
                     if Envir.aeconv (red ph' is [], t) then
                       Seq.single (env, Unification_Base.reflexive_term ctxt
                         (Binders.replace_binders binders t))
                     else raise FALLBACK
               end
           | (ph, ps) =>
               let val (th, ts) = strip_comb t
               in case (ph, th) of
                   (Abs _, _) => raise Unification_Base.PATTERN
                 | (_, Abs _) => raise Unification_Base.PATTERN
                 | _ => if null ps orelse null ts then raise FALLBACK
                     else (*Note: types of theorems are already normalised
                       ==> we pass the identity type normaliser*)
                       Util.strip_comb_strip_comb (K o K I) match binders ctxt (ph, th) (ps, ts) env
                       |> seq_try
               end)
         handle FALLBACK => handle_failure match_theory_fail
           (fn _ => Pretty.str "Higher-order pattern matching failed.")
         | Unification_Base.PATTERN => handle_failure match_theory_pattern
           (fn _ => Pretty.str "Terms not in Pattern fragment.")
       end
   in
     (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "Higher-order pattern matching ",
         Util.pretty_unif_problem ctxt (norm_pt env pt)
       ] |> Pretty.string_of);
     match binders ctxt pt env)
     handle Unification_Base.UNIF => Seq.empty (*types do not match*)
   end
 
 (*standard higher-order pattern matching*)
 val match = e_match Util.match_types Unification_Combinator.fail_match
   Unification_Combinator.fail_match
 
 (*unification*)
 
 fun string_of_term ctxt env binders t =
   (map (Free o fst) binders, t)
   |> subst_bounds
   |> Norm.norm_term_unif env
   |> Syntax.string_of_term ctxt
 
 fun bname binders = fst o fst o nth binders
 fun bnames binders is = map (bname binders) is |> space_implode " "
 
 fun proj_fail ctxt (env, binders, F, _, is, t) reason =
   @{log Logger.DEBUG} ctxt (fn _ =>
     let
       val f = Term.string_of_vname F
       val xs = bnames binders is
       val u = string_of_term ctxt env binders t
     in
       cat_lines [
         "Cannot unify variable " ^ f ^ " (depending on bound variables [" ^ xs ^ "])",
         "with term " ^ u,
         reason ()
       ]
     end)
 
 fun proj_fail_unif ctxt (params as (_, binders, _, _, is, t)) =
   let
     fun reason () =
       let val ys = bnames binders (subtract (op =) is (loose_bnos t))
       in "Term contains additional bound variable(s) " ^ ys end
   in proj_fail ctxt params reason end
 
 fun proj_fail_type_app ctxt (params as (env, binders, _, _, _, _)) var_app =
   let
     fun reason () =
       let val var_app = string_of_term ctxt env binders var_app
       in "Projection " ^ var_app ^ " is not well-typed." end
   in proj_fail ctxt params reason end
 
 fun ocheck_fail ctxt (F, t, binders, env) =
   @{log Logger.DEBUG} ctxt (fn _ => cat_lines [
       "Variable " ^ Term.string_of_vname F ^ " occurs in term",
       string_of_term ctxt env binders t,
       "Cannot unify!"
     ])
 
 fun occurs (F, t, env) =
   let fun occ (Var (G, T)) = (case Envir.lookup env (G, T) of
             SOME t => occ t
           | NONE => F = G)
         | occ (t1 $ t2) = occ t1 orelse occ t2
         | occ (Abs (_, _, t)) = occ t
         | occ _ = false
   in occ t end
 
 fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts)
 
 (*split_type ([T1,....,Tn]---> T) n = ([Tn,...,T1], T)*)
 fun split_type t n =
   let fun split (T, 0, Ts) = (Ts, T)
         | split (Type ("fun", [T1, T2]), n, Ts) = split (T2, n - 1, T1 :: Ts)
         | split _ = raise Fail "split_type"
   in split (t, n, []) end
 
 fun type_of_G (Envir.Envir {tyenv,...}) (T, n, is) =
   let val (Ts, U) = split_type (Norm.norm_type_unif tyenv T) n
   in map (nth Ts) is ---> U end
 
 fun mk_hnf (binders, is, G, js) = mkabs (binders, is, app (G, js))
 
 fun mk_new_hnf (env, binders, is, F as (a, _), T, js) =
   let val (env', G) = Envir.genvar a (env, type_of_G env (T, length is, js))
   in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end
 
 (*mk_proj_list is = [ |is| - k - 1 | 0 <= k < |is| and is[k] >= 0 ]*)
 fun mk_proj_list is =
   let fun mk (SOME _) (acc, j) = (j :: acc, j + 1)
         | mk NONE (acc, j) = (acc, j + 1)
   in fold_rev mk is ([], 0) |> fst end
 
 fun proj ctxt (s, env, binders, is) =
   let
     fun trans d i = if i < d then i else idx is (i - d) + d
     fun pr (s, env, d, binders) = (case Envir.head_norm env s of
         Abs (a, T, t) =>
           let
             val (binder, _) = Binders.fix_binder (a, T) ctxt
             val (t', env') = pr (t, env, d + 1, binder :: binders)
           in (Abs (a, T, t'), env') end
       | t => (case strip_comb t of
           (c as Const _, ts) =>
             let val (ts', env') = prs (ts, env, d, binders)
             in (list_comb (c, ts'), env') end
         | (f as Free _, ts) =>
             let val (ts', env') = prs (ts, env, d, binders)
             in (list_comb (f, ts'), env') end
         | (Bound i, ts) =>
             let
               val j = trans d i
               val (ts', env') = prs (ts, env, d, binders)
             in (list_comb (Bound j, ts'), env') end
         | (Var (F as (a, _), Fty), ts) =>
             let
               val js = ints_of' env ts
               val js' = map (try (trans d)) js
               val ks = mk_proj_list js'
               val ls = map_filter I js'
               val Hty = type_of_G env (Fty, length js, ks)
               val (env', H) = Envir.genvar a (env, Hty)
               val env'' = Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env'
             in (app (H, ls), env'') end
         | _  => raise Unification_Base.PATTERN))
     and prs (s :: ss, env, d, binders) =
           let
             val (s', env1) = pr (s, env, d, binders)
             val (ss', env2) = prs (ss, env1, d, binders)
           in (s' :: ss', env2) end
       | prs ([], env, _, _) = ([], env)
   in
     if downto0 (is, length binders - 1) then (s, env)
     else pr (s, env, 0, binders)
   end
 
 (*mk_ff_list (is, js) = [ |is| - k - 1 | 0 <= k < |is| and is[k] = js[k] ]*)
 fun mk_ff_list (is,js) =
     let fun mk ([], [], _) = []
           | mk (i :: is, j :: js, k) =
               if i = j then k :: mk (is, js, k - 1)
               else mk (is, js, k - 1)
           | mk _ = raise Fail "mk_ff_list"
     in mk (is, js, length is - 1) end;
 
 fun app_free (Envir.Envir {tyenv,...}) binders n T is =
   let val norm_type = Norm.norm_type_unif tyenv
   in list_comb (Var (n, norm_type T), map (map_types norm_type o Binders.nth_binder_data binders) is) end
 
 fun flexflex1 unify_types ctxt (env, binders, F, Fty, Fty', is, js) =
   let
     val env' = unify_types ctxt (Fty, Fty') env
     val thm = app_free env binders F Fty is |> Unification_Base.reflexive_term ctxt
   in
     if is = js then (env', thm)
     else
       let
         val ks = mk_ff_list (is, js)
         val env'' = mk_new_hnf (env', binders, is, F, Fty, ks)
       in (env'', thm) end
   end
 
 fun flexflex2 unify_types ctxt (env, binders, F, Fty, is, G, Gty, js) =
   let
     val var_app = app_free env binders F Fty is
     val binder_types = Binders.binder_types binders
     val env' = unify_types ctxt
       (apply2 (Envir.fastype env binder_types) (var_app, app (Var (G, Gty), js))) env
     val thm = Unification_Base.reflexive_term ctxt var_app
     fun ff (F, Fty, is, G as (a, _), Gty, js) =
       if subset (op =) (js, is) then
         let
           val t = mkabs (binders, is, app (Var (G, Gty), map (idx is) js))
           val env'' = Envir.update ((F, Fty), t) env'
         in (env'', thm) end
       else
         let
           val ks = inter (op =) js is
           val Hty = type_of_G env' (Fty, length is, map (idx is) ks)
           val (env'', H) = Envir.genvar a (env', Hty)
           fun lam is = mkabs (binders, is, app (H, map (idx is) ks))
           val env''' =
             Envir.update ((F, Fty), lam is) env''
             |> Envir.update ((G, Gty), lam js)
         in (env''', thm) end
   in
     if is_less (Term_Ord.indexname_ord (G, F)) then ff (F, Fty, is, G, Gty, js)
     else ff (G, Gty, js, F, Fty, is)
   end
 
 fun flexrigid unify_types ctxt (params as (env, binders, F, Fty, is, t)) =
   if occurs (F, t, env) then (ocheck_fail ctxt (F, t, binders, env); raise FALLBACK)
   else
     let val var_app = app_free env binders F Fty is
     in
       let
         val binder_types = Binders.binder_types binders
         val env' = unify_types ctxt
           (apply2 (Envir.fastype env binder_types) (var_app, t)) env
         val (u, env'') = proj ctxt (t, env', binders, is)
         val env''' = Envir.update ((F, Fty), mkabs (binders, is, u)) env''
         val thm = Unification_Base.reflexive_term ctxt var_app
       in (env''', thm) end
       handle IDX => (proj_fail_unif ctxt params; raise OPEN_TERM)
       | TYPE _ => (proj_fail_type_app ctxt params var_app; raise Unification_Base.UNIF)
     end
 
 (** higher-order pattern E-unification **)
 val norms_unify = Util.beta_eta_short_norms_unif
 
 fun e_unify unify_types unify_theory_pattern unify_theory_fail binders ctxt st env =
   let
     fun unif binders ctxt st env =
       let
         val (st' as (s', t')) = apply2 (Envir.head_norm env) st
         fun rigid_rigid ctxt t n env = (*we do not normalise types in base cases*)
           Util.rigid_rigid (K I) unify_types ctxt t n env |> seq_try
           handle Unification_Base.UNIF => Seq.empty (*types do not match*)
         (*call unify_theory on failure*)
         fun handle_failure unify_theory failure_msg =
           (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [
             failure_msg (),
             Util.pretty_call_theory_unif ctxt st'
           ] |> Pretty.block |> Pretty.string_of);
           (*Note: st' is already normalised*)
           unify_theory binders ctxt st' env)
       in
         (case st' of
           (Abs (ns, Ts, ts), Abs (nt, Tt, tt)) =>
             ((let val name = if ns = "" then nt else ns
             in
               unify_types ctxt (Ts, Tt) env
               |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt name Ts (ts, tt)
               |> seq_try
             end)
             handle Unification_Base.UNIF => Seq.empty) (*types do not unify*)
         (*eta-expand on the fly*)
         | (Abs (ns, Ts, ts), _) =>
             ((let val st = apply2 (Envir.fastype env (Binders.binder_types binders)) st'
             in
               unify_types ctxt st env
               |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt ns Ts
                 (ts, incr_boundvars 1 t' $ Bound 0)
               |> seq_try
             end)
             handle Unification_Base.UNIF => Seq.empty) (*types do not unify*)
         | (_, Abs _) => unif binders ctxt (t', s') env |> Seq.map (apsnd Unification_Base.symmetric)
         | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env)
         | (Free _, Free g) => rigid_rigid ctxt s' g env
         | (Const _, Const d) => rigid_rigid ctxt s' d env
         (*case distinctions on head term*)
         | _ => case apply2 strip_comb st' of
             ((Var (F, Fty), ss), (Var (G, Gty), ts)) =>
               (((if F = G then
                 flexflex1 unify_types ctxt (env, binders, F, Fty, Gty, ints_of' env ss, ints_of' env ts)
               else
                 flexflex2 unify_types ctxt (env, binders, F, Fty, ints_of' env ss, G, Gty, ints_of' env ts))
               |> Seq.single)
               handle Unification_Base.UNIF => Seq.empty) (*types do not unify*)
           | ((Var (F, Fty), ss), _) =>
               (flexrigid unify_types ctxt (env, binders, F, Fty, ints_of' env ss, t')|> Seq.single
               handle OPEN_TERM => Seq.empty
               | Unification_Base.UNIF => Seq.empty) (*types do not unify*)
           | (_, (Var (F, Fty), ts)) =>
               (flexrigid unify_types ctxt (env, binders, F, Fty, ints_of' env ts, s') |> Seq.single
               handle OPEN_TERM => Seq.empty
               | Unification_Base.UNIF => Seq.empty) (*types do not unify*)
           | ((sh, ss), (th, ts)) => if null ss orelse null ts then raise FALLBACK
               else (*but we have to normalise in comb cases*)
                 Util.strip_comb_strip_comb Norm.norm_thm_types_unif unif binders ctxt
                   (sh, th) (ss, ts) env
                 |> seq_try)
         handle FALLBACK => handle_failure unify_theory_fail
           (fn _ => Pretty.str "Higher-order pattern unification failed.")
         | Unification_Base.PATTERN => handle_failure unify_theory_pattern
           (fn _ => Pretty.str "Terms not in Pattern fragment.")
       end
   in
     (@{log Logger.DEBUG} ctxt (fn _ =>
       Pretty.block [
         Pretty.str "Higher-order pattern unifying ",
         Util.pretty_unif_problem ctxt (apply2 (Norm.norm_term_unif env) st)
-      ]
-      |> Pretty.string_of);
+      ] |> Pretty.string_of);
     unif binders ctxt st env)
     handle Unification_Base.UNIF => Seq.empty (*types do not unify*)
   end
 
 (*standard higher-order pattern unification*)
 val unify = e_unify Util.unify_types Unification_Combinator.fail_unify
   Unification_Combinator.fail_unify
 
 end
diff --git a/thys/ML_Unification/Unifiers/higher_order_unification.ML b/thys/ML_Unification/Unifiers/higher_order_unification.ML
--- a/thys/ML_Unification/Unifiers/higher_order_unification.ML
+++ b/thys/ML_Unification/Unifiers/higher_order_unification.ML
@@ -1,53 +1,53 @@
 (*  Title:      ML_Unification/higher_order_unification.ML
     Author:     Kevin Kappelmann TU Muenchen
 
 Higher-order unification from the Pure kernel adjusted to fit the
 Unification_Base.unifier type, i.e. moving flex-flex pairs into the theorem
 and support of open term unification.
 *)
 
 signature HIGHER_ORDER_UNIFICATION =
 sig
   include HAS_LOGGER
 
   val unify : Unification_Base.unifier
   val norms : Unification_Base.normalisers
 end
 
 structure Higher_Order_Unification : HIGHER_ORDER_UNIFICATION =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Higher_Order_Unification"
 
 structure Util = Unification_Util
 
+val norms = Unification_Util.beta_eta_short_norms_unif
+
 val unify =
   let fun unif binders ctxt tp env =
     let
       val _ = @{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
           Pretty.str "Higher-order unifying ",
           Util.pretty_unif_problem ctxt (apply2 (Envir.norm_term env) tp)
         ] |> Pretty.string_of)
       val init_goal = Logic.mk_equals #> Thm.cterm_of ctxt #> Goal.init
       fun create_env_thmq env =
         (*replace binders and apply the computed unifier*)
-        apply2 (Envir_Normalisation.beta_eta_short_norm_term_unif env o Binders.replace_binders binders) tp
+        apply2 (Binders.replace_binders binders #> (#inst_term norms env #> #norm_term norms)) tp
         (*create a goal such that we can create a theorem including the flex-flex pairs*)
         |> init_goal
         (*kind of a hack: resolving against the equality theorem will add the
           flex-flex pairs to the theorem*)
         |> HEADGOAL (match_tac ctxt @{thms Pure.reflexive})
         (*conclude the goal and pair with the environment*)
         |> Seq.map (pair env o Goal.conclude)
     in
       (*find the unifiers*)
       Unify.hounifiers (map fst binders) (Context.Proof ctxt, env, [tp])
       (*add the flex-flex pairs to the theorem*)
       |> Seq.maps (create_env_thmq o fst)
     end
   in Type_Unification.e_unify Util.unify_types unif end
 
-val norms = Unification_Util.beta_eta_short_norms_unif
-
 end
 
diff --git a/thys/ML_Unification/Unifiers/simplifier_unification.ML b/thys/ML_Unification/Unifiers/simplifier_unification.ML
--- a/thys/ML_Unification/Unifiers/simplifier_unification.ML
+++ b/thys/ML_Unification/Unifiers/simplifier_unification.ML
@@ -1,107 +1,112 @@
 (*  Title:      ML_Unification/simplifier_unification.ML
     Author:     Kevin Kappelmann
 
 Solving equations for unification problems with the simplifier.
 *)
 signature SIMPLIFIER_UNIFICATION =
 sig
   include HAS_LOGGER
   (*solves "SIMPS_TO s t \<equiv> rhs" via simplification of s when given a theorem
     "SIMPS_TO s t \<Longrightarrow> SIMPS_TO s t \<equiv> rhs"*)
   val SIMPS_TO_unify : thm -> Unification_Base.closed_unifier
   (*solves "SIMPS_TO_UNIF s t \<equiv> rhs" via simplification of s to s', followed by unification of
     "s' \<equiv>\<^sup>? t", when given a theorem "SIMPS_TO_UNIF s t \<Longrightarrow> SIMPS_TO_UNIF s t \<equiv> rhs"*)
   val SIMPS_TO_UNIF_unify : thm -> Unification_Base.normalisers ->
     Unification_Base.closed_unifier -> Unification_Base.closed_unifier
   (*solves "s \<equiv>\<^sup>? t" via simplification followed by unification*)
   val simp_unify : Unification_Base.normalisers -> Unification_Base.closed_unifier ->
     Unification_Base.closed_unifier
   (*solves "s \<equiv>\<^sup>? t" via simplification followed by unification; aborts if no progress was made
   during simplification*)
   val simp_unify_progress : (term * term -> bool) -> (Unification_Base.normalisers ->
     Unification_Base.closed_unifier -> Unification_Base.closed_unifier) ->
     Envir_Normalisation.term_normaliser -> Unification_Base.normalisers ->
     Unification_Base.e_unifier
 end
 
 structure Simplifier_Unification : SIMPLIFIER_UNIFICATION =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Simplifier_Unification"
 
 structure Util = Tactic_Util
 
 (*some "safe" solvers create instantiations via flex-flex pairs, which we disallow*)
 val safe_simp_tac = Util.safe_simp_tac
 
 fun match_tac ctxt = Tactic.match_tac ctxt o single
 
 fun SIMPS_TO_unify preprocess_rule ctxt =
   let fun tac (tp as (lhs, _)) =
     if can Simps_To.dest_SIMPS_TO lhs
     then
       (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
           Pretty.str "Solving ",
           Syntax.pretty_term ctxt @{term SIMPS_TO},
           Pretty.str " unification problem ",
           Unification_Util.pretty_unif_problem ctxt tp
         ] |> Pretty.string_of);
       match_tac ctxt preprocess_rule
       THEN' Simps_To.SIMPS_TO_tac (safe_simp_tac ctxt) ctxt)
     else K no_tac
   in Tactic_Unification.unify (Tactic_Unification.env_tac_from_no_inst_tac o tac) ctxt end
 
 fun SIMPS_TO_UNIF_env_thm_tac norms unif ctxt env tSIMPS_TO_UNIF state =
   let
     val tp = Simps_To_Unif.dest_SIMPS_TO_UNIF tSIMPS_TO_UNIF
-    fun norm_resolve (env, thm) = #norm_thm norms ctxt env state |> Thm.elim_implies thm |> pair env
+    val conv = #conv norms
+    fun norm_resolve (env, thm) =
+      Tactic_Util.HEADGOAL (Unification_Util.inst_norm_subgoal (#inst_unif_thm norms) conv)
+        ctxt env state
+      |> Thm.elim_implies (Conversion_Util.apply_thm_conv conv thm)
+      |> pair env
   in
     Simps_To_Unif.SIMPS_TO_UNIF_env_thmsq (safe_simp_tac ctxt) norms unif ctxt tp env
     |> Seq.map norm_resolve
   end
 
 fun SIMPS_TO_UNIF_unify preprocess_rule norms unif ctxt =
   let fun tac (tp as (lhs, _)) i (env, state) =
     if can Simps_To_Unif.dest_SIMPS_TO_UNIF lhs
     then
       (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
           Pretty.str "Solving ",
           Syntax.pretty_term ctxt @{term SIMPS_TO_UNIF},
           Pretty.str " unification problem ",
           Unification_Util.pretty_unif_problem ctxt tp
         ] |> Pretty.string_of);
       match_tac ctxt preprocess_rule i state
       |> Seq.maps (SIMPS_TO_UNIF_env_thm_tac norms unif ctxt env lhs))
     else Seq.empty
   in Tactic_Unification.unify tac ctxt end
 
 fun simp_unify norms unif ctxt =
   let
     val simp_tac = safe_simp_tac ctxt
     fun SIMPS_TO_UNIF_env_thm_tac' env i state = SIMPS_TO_UNIF_env_thm_tac norms unif ctxt env
       (Thm.cprem_of state i |> Thm.term_of) state
     fun eq_tac tp i (env, state) =
       (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "Solving unification problem via simplification followed by unification ",
         Unification_Util.pretty_unif_problem ctxt tp
       ] |> Pretty.string_of);
       Util.THEN' (
       match_tac ctxt @{thm eq_if_SIMPS_TO_UNIF_if_SIMPS_TO}
       THEN' Simps_To.SIMPS_TO_tac (Simps_To.simp_inst_tac simp_tac) ctxt,
       SIMPS_TO_UNIF_env_thm_tac' env) i state)
   in Tactic_Unification.unify eq_tac ctxt end
 
 fun simp_unify_progress teq simp_unify norm_term norms unif binders ctxt tp env =
   let
     val tp as (lhs, rhs) = apply2 (Binders.replace_binders binders #> norm_term env) tp
     fun unify ctxt (tp' as (lhs', rhs')) = if teq (lhs, lhs') andalso teq (rhs, rhs')
       then (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
           Pretty.str "Simplification of ",
           Unification_Util.pretty_unif_problem ctxt tp,
           Pretty.str " failed (no progress)"
         ] |> Pretty.string_of);
         K Seq.empty)
       else unif binders ctxt (apply2 (Binders.replace_frees binders) tp')
   in simp_unify norms unify ctxt tp env end
 
 end
diff --git a/thys/ML_Unification/unification_base.ML b/thys/ML_Unification/unification_base.ML
--- a/thys/ML_Unification/unification_base.ML
+++ b/thys/ML_Unification/unification_base.ML
@@ -1,77 +1,87 @@
 (*  Title:      ML_Unification/unification_base.ML
     Author:     Kevin Kappelmann
 
 Basic definitions for unifiers.
 *)
 signature UNIFICATION_BASE =
 sig
   include HAS_LOGGER
 
   val reflexive : cterm -> thm
   val combination : thm -> thm -> thm
   val symmetric : thm -> thm
   val abstract_rule : Proof.context -> string -> cterm -> thm -> thm option
   val reflexive_term : Proof.context -> term -> thm
 
   (*raised on unsupported input*)
   exception PATTERN
 
   (*raised on unification failure for non-sequence outputs (e.g. type unification)*)
   exception UNIF
 
   type type_unifier = Proof.context -> typ * typ -> Envir.env -> Envir.env
   type type_matcher = type_unifier
 
   type closed_unifier = Proof.context -> term * term -> Envir.env -> (Envir.env * thm) Seq.seq
   (*term binders stores fresh free variables associated to each loose bound variable*)
   type unifier = term Binders.binders -> closed_unifier
   type e_unifier = unifier -> unifier
 
   type closed_matcher = closed_unifier
   type matcher = unifier
   type e_matcher = matcher -> matcher
 
-  (* normalisers for matchers/unifiers *)
+  (* normalisers for matching/unification results (\<sigma>, lhs \<equiv> rhs) of terms t1 \<equiv>\<^sup>? t2:
+  it must hold (ignoring conversions between terms and theorems) that
+  - inst_unif_thm(\<sigma>, lhs \<equiv> rhs) \<equiv>\<^sub>\<alpha>\<^sub>\<beta>\<^sub>\<eta> (inst_term(\<sigma>, t1) \<equiv> inst_term(\<sigma>, t2))
+  - norm_term(inst_unif_thm(\<sigma>, lhs \<equiv> rhs)) \<equiv>\<^sub>\<alpha> norm_term(inst_term(\<sigma>, t1) \<equiv> inst_term(\<sigma>, t2))
+  *)
   type normalisers = {
-    (*normaliser for result of unifier*)
-    norm_unif_thm : Envir_Normalisation.thm_normaliser,
-    (*normaliser for other theorems*)
-    norm_thm : Envir_Normalisation.thm_normaliser,
-    (*normaliser for terms*)
-    norm_term : Envir_Normalisation.term_normaliser
+    (*instantiation for equality theorem of unifier*)
+    inst_unif_thm : Envir_Normalisation.thm_normaliser,
+    (*instantiation for terms*)
+    inst_term : Envir_Normalisation.term_normaliser,
+    (*instantiation for theorems corresponding to inst_term*)
+    inst_thm : Envir_Normalisation.thm_normaliser,
+    (*normalisation for terms*)
+    norm_term : Term_Normalisation.term_normaliser,
+    (*normalisation conversion corresponding to norm_term*)
+    conv : conv
   }
 
 end
 
 structure Unification_Base : UNIFICATION_BASE =
 struct
 
 val logger = Logger.setup_new_logger Logger.root "Unification_Base"
 
 val reflexive = Thm.reflexive
 val combination = Thm.combination
 val symmetric = Thm.symmetric
 val abstract_rule = Thm_Util.abstract_rule
 
 val reflexive_term = reflexive oo Thm.cterm_of
 
 exception PATTERN = Pattern.Pattern
 
 exception UNIF = Pattern.Unif
 type type_unifier = Proof.context -> typ * typ -> Envir.env -> Envir.env
 type type_matcher = type_unifier
 type closed_unifier = Proof.context -> term * term -> Envir.env ->
   (Envir.env * thm) Seq.seq
 type unifier = term Binders.binders -> closed_unifier
 type e_unifier = unifier -> unifier
 type closed_matcher = closed_unifier
 type matcher = unifier
 type e_matcher = matcher -> matcher
 
 type normalisers = {
-  norm_unif_thm : Envir_Normalisation.thm_normaliser,
-  norm_thm : Envir_Normalisation.thm_normaliser,
-  norm_term : Envir_Normalisation.term_normaliser
+  inst_unif_thm : Envir_Normalisation.thm_normaliser,
+  inst_term : Envir_Normalisation.term_normaliser,
+  inst_thm : Envir_Normalisation.thm_normaliser,
+  norm_term : Term_Normalisation.term_normaliser,
+  conv : conv
 }
 
 end
diff --git a/thys/ML_Unification/unification_util.ML b/thys/ML_Unification/unification_util.ML
--- a/thys/ML_Unification/unification_util.ML
+++ b/thys/ML_Unification/unification_util.ML
@@ -1,306 +1,300 @@
 (*  Title:      ML_Unification/unification_util.ML
     Author:     Kevin Kappelmann
 
 Utilities used for e-unifications.
 *)
 signature UNIFICATION_UTIL =
 sig
   include HAS_LOGGER
 
   (* pretty-printing *)
   val pretty_types : Proof.context -> typ list -> Pretty.T
   val pretty_terms : Proof.context -> term list -> Pretty.T
 
   val pretty_tyenv : Proof.context -> Type.tyenv -> Pretty.T
   val pretty_tenv : Proof.context -> Envir.tenv -> Pretty.T
   val pretty_env : Proof.context -> Envir.env -> Pretty.T
 
   val pretty_unif_problem : Proof.context -> (term * term) -> Pretty.T
   val pretty_unif_result : Proof.context -> (Envir.env * thm) -> Pretty.T
 
   val pretty_call_theory_match : Proof.context -> (term * term) -> Pretty.T
   val pretty_call_theory_unif : Proof.context -> (term * term) -> Pretty.T
 
   (* terms and environments *)
   val maxidx_of_terms : term list -> int
   (*returns empty environment with maxidx set to maximum of given terms*)
   val empty_envir : term * term -> Envir.env
 
   (* type unification *)
 
   (*raises Unification_Base.UNIF on failure*)
   val unify_types : Unification_Base.type_unifier
   (*raises Unification_Base.UNIF on failure*)
   val match_types : Unification_Base.type_matcher
 
   (* normalisers *)
   val eta_short_norms_match : Unification_Base.normalisers
   val beta_eta_short_norms_match : Unification_Base.normalisers
   val eta_short_norms_unif : Unification_Base.normalisers
   val beta_eta_short_norms_unif : Unification_Base.normalisers
 
+  val inst_norm_term : Envir_Normalisation.term_normaliser -> Term_Normalisation.term_normaliser ->
+    Envir_Normalisation.term_normaliser
+  val inst_norm_term' : Unification_Base.normalisers -> Envir_Normalisation.term_normaliser
+  val inst_norm_thm : Envir_Normalisation.thm_normaliser -> conv ->
+    Envir_Normalisation.thm_normaliser
+  val inst_norm_subgoal : Envir_Normalisation.thm_normaliser -> conv -> int ->
+    Envir_Normalisation.thm_normaliser
+
   (* shared standard cases for unifiers *)
   val smash_tpairs_if_occurs : Proof.context -> term -> Envir.env * thm -> (Envir.env * thm) Seq.seq
   val abstract_abstract : Envir_Normalisation.term_type_normaliser -> Unification_Base.unifier ->
     term Binders.binders -> Proof.context -> string -> typ ->
     (term * term) -> Envir.env -> (Envir.env * thm) Seq.seq
   (*raises UNIF if types do not unify*)
   val rigid_rigid : Envir_Normalisation.term_type_normaliser -> Unification_Base.type_unifier ->
     Proof.context -> term -> (string * typ) -> Envir.env -> (Envir.env * thm) Seq.seq
   val bound_bound : term Binders.binders -> Proof.context -> (int * int) ->
     thm Seq.seq
   val comb_comb : Envir_Normalisation.thm_type_normaliser -> Unification_Base.closed_unifier ->
     Proof.context -> (term * term) -> (term * term) -> Envir.env -> (Envir.env * thm) Seq.seq
   val args_args : Envir_Normalisation.thm_type_normaliser -> Unification_Base.closed_unifier ->
     Proof.context -> (term list * term list) -> (Envir.env * thm) Seq.seq -> (Envir.env * thm) Seq.seq
   val strip_comb_strip_comb : Envir_Normalisation.thm_type_normaliser -> Unification_Base.unifier ->
     term Binders.binders -> Proof.context -> (term * term) ->
     (term list * term list) -> Envir.env -> (Envir.env * thm) Seq.seq
 
   (* logging *)
   val log_unif_result : Proof.context -> term * term -> Envir.env * thm -> unit
   val log_unif_results : Proof.context -> term * term -> Unification_Base.closed_unifier -> unit
   val log_unif_results' : int -> Proof.context  -> term * term -> Unification_Base.closed_unifier -> unit
 
 end
 
 structure Unification_Util : UNIFICATION_UTIL =
 struct
 
 val logger = Logger.setup_new_logger Unification_Base.logger "Util"
 
 structure Norm = Envir_Normalisation
 structure UBase = Unification_Base
+structure Show = SpecCheck_Show_Term
 
 (* pretty-printing *)
-local
-val pretty_term = Syntax.pretty_term
-val pretty_type = Syntax.pretty_typ
-
-fun pretty_env_aux show_entry =
-  Vartab.dest
-  #> map show_entry
-  #> Pretty.list "[" "]"
-
-fun pretty_env_entry show (s, t) = Pretty.block [show s, Pretty.str " := ", show t]
-
-val pretty_record =
-  map (fn (key, entry) => Pretty.block [Pretty.str key, Pretty.str "=", entry])
-  #> Pretty.enum "," "{" "}"
-in
-
-fun pretty_types ctxt = Pretty.block o Pretty.commas o map (pretty_type ctxt)
-fun pretty_terms ctxt = Pretty.block o Pretty.commas o map (pretty_term ctxt)
+val pretty_term = Show.term
+val pretty_type = Show.typ
 
-fun pretty_tyenv ctxt =
-  let
-    val show_entry = pretty_env_entry (pretty_type ctxt)
-    fun get_typs (v, (s, T)) = (TVar (v, s), T)
-  in pretty_env_aux (show_entry o get_typs) end
+fun pretty_commas show = Pretty.block o Pretty.commas o map show
+val pretty_types = pretty_commas o pretty_type
+val pretty_terms = pretty_commas o pretty_term
 
-fun pretty_tenv ctxt =
-  let
-    val show_entry = pretty_env_entry (pretty_term ctxt)
-    fun get_trms (v, (T, t)) = (Var (v, T), t)
-  in pretty_env_aux (show_entry o get_trms) end
-
-fun pretty_env ctxt (Envir.Envir {maxidx, tyenv, tenv}) =
-  pretty_record [
-    ("maxidx", Pretty.str (string_of_int maxidx)),
-    ("tyenv", pretty_tyenv ctxt tyenv),
-    ("tenv", pretty_tenv ctxt tenv)
-  ]
-
-end
+val pretty_tyenv = Show.tyenv
+val pretty_tenv = Show.tenv
+val pretty_env = Show.env
 
 fun pretty_unif_problem ctxt (t1, t2) =
-  Pretty.block [pretty_terms ctxt [t1], Pretty.str " \<equiv>\<^sup>? " , pretty_terms ctxt [t2]]
+  Pretty.block [pretty_term ctxt t1, Pretty.str " \<equiv>\<^sup>? " , pretty_term ctxt t2]
 
 fun pretty_unif_result ctxt (env, thm) = Pretty.block [
     Pretty.str "Environment: ",
     pretty_env ctxt env,
     Pretty.fbrk,
     Pretty.str "Theorem: ",
     Thm.pretty_thm ctxt thm
   ]
 
 fun pretty_call_theory_match ctxt pt = Pretty.block [
     Pretty.str "Calling theory matcher for ",
     pretty_unif_problem ctxt pt
   ]
 
 fun pretty_call_theory_unif ctxt tp = Pretty.block [
     Pretty.str "Calling theory unifier for ",
     pretty_unif_problem ctxt tp
   ]
 
 (* terms and environments *)
 fun maxidx_of_terms ts = fold (Integer.max o maxidx_of_term) ts ~1
 
 fun empty_envir (t1, t2) = Envir.empty (maxidx_of_terms [t1, t2])
 
 (* type unification *)
 
 fun match_types ctxt (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   (if pointer_eq (T, U) then env
   else
     let val tyenv' = Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
     in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv'} end)
   handle Type.TYPE_MATCH =>
     (@{log Logger.DEBUG} ctxt
       (fn _ => Pretty.block [
           Pretty.str "Failed to match types ",
           pretty_types ctxt [Envir_Normalisation.norm_type_match tyenv T, U]
         ] |> Pretty.string_of);
     raise UBase.UNIF)
 
 fun unify_types ctxt (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   (if pointer_eq (T, U) then env
   else
     let val (tyenv', maxidx') =
       Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx)
     in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end)
   handle Type.TUNIFY =>
     (@{log Logger.DEBUG} ctxt
       (fn _ => Pretty.block [
           Pretty.str "Failed to unify types ",
           pretty_types ctxt (map (Envir_Normalisation.norm_type_unif tyenv) [T, U])
         ] |> Pretty.string_of);
     raise UBase.UNIF)
 
 (* normalisers *)
 val eta_short_norms_match = {
-  (*Precondition: the matcher must already normalise the types in its theorem!*)
-  norm_unif_thm = Norm.eta_short_norm_thm (K I) Norm.eta_short_norm_term_match,
-  norm_thm = Norm.eta_short_norm_thm_match,
-  norm_term = Norm.eta_short_norm_term_match
+  (*Precondition: the matcher must already instantiate its theorem!*)
+  inst_unif_thm = K o K I,
+  inst_term = Norm.norm_term_match,
+  inst_thm = Norm.norm_thm_match,
+  norm_term = Term_Normalisation.eta_short,
+  conv = Conversion_Util.eta_short_conv
 }
 val beta_eta_short_norms_match = {
   (*Precondition: the matcher must already normalise the types in its theorem!*)
-  norm_unif_thm = Norm.beta_eta_short_norm_thm (K I) Norm.beta_eta_short_norm_term_match,
-  norm_thm = Norm.beta_eta_short_norm_thm_match,
-  norm_term = Norm.beta_eta_short_norm_term_match
+  inst_unif_thm = (#inst_unif_thm eta_short_norms_match),
+  inst_term = (#inst_term eta_short_norms_match),
+  inst_thm = (#inst_thm eta_short_norms_match),
+  norm_term = Term_Normalisation.beta_eta_short,
+  conv = Conversion_Util.beta_eta_short_conv
 }
+
 val eta_short_norms_unif = {
-  norm_unif_thm = Norm.eta_short_norm_thm_unif,
-  norm_thm = Norm.eta_short_norm_thm_unif,
-  norm_term = Norm.eta_short_norm_term_unif
+  inst_unif_thm = Norm.norm_thm_unif,
+  inst_term = Norm.norm_term_unif,
+  inst_thm = Norm.norm_thm_unif,
+  norm_term = Term_Normalisation.eta_short,
+  conv = Conversion_Util.eta_short_conv
 }
 val beta_eta_short_norms_unif = {
-  norm_unif_thm = Norm.beta_eta_short_norm_thm_unif,
-  norm_thm = Norm.beta_eta_short_norm_thm_unif,
-  norm_term = Norm.beta_eta_short_norm_term_unif
+  inst_unif_thm = (#inst_unif_thm eta_short_norms_unif),
+  inst_term = (#inst_term eta_short_norms_unif),
+  inst_thm = (#inst_thm eta_short_norms_unif),
+  norm_term = Term_Normalisation.beta_eta_short,
+  conv = Conversion_Util.beta_eta_short_conv
 }
 
+fun inst_norm_term inst_term norm_term = norm_term oo inst_term
+fun inst_norm_term' norms = inst_norm_term (#inst_term norms) (#norm_term norms)
+fun inst_norm_thm inst_thm conv = Conversion_Util.apply_thm_conv conv ooo inst_thm
+fun inst_norm_subgoal inst_thm conv i = Conversion_Util.apply_subgoal_conv conv i ooo inst_thm
+
 (* shared standard cases for unifiers *)
 fun smash_tpairs_if_occurs ctxt t (env, thm) =
   let
     val tpairs = Thm.tpairs_of thm
     fun occs_t s = Logic.occs (t, s)
   in
     if exists (fn (t1, t2) => occs_t t1 orelse occs_t t2) tpairs
     then
       let
         (*in a perfect world, we would make the relevant tpairs of the theorem
           equality premises that can be solved by an arbitrary solver;
           however, Isabelle's kernel only allows one to solve tpairs
           with the built-in higher-order (pattern) unifier.*)
         (*only the kernel HO-unifier may add flex-flex pairs -> safe to normalise wrt. unification*)
         val normed_thm = Norm.norm_thm_unif ctxt env thm
         val normed_tpairs = Thm.tpairs_of normed_thm
       in
         (*note: we need to use the same unifier and environment as Thm.flexflex_rule here so that
           the final environment and theorem agree*)
         Unify.smash_unifiers (Context.Proof ctxt) normed_tpairs
           (Envir.empty (Thm.maxidx_of normed_thm))
         |> Seq.maps (fn smash_env =>
           (let val new_env = Envir.merge (smash_env, env)
           in Thm.flexflex_rule (SOME ctxt) normed_thm |> Seq.map (pair new_env) end)
           handle Vartab.DUP _ => (@{log Logger.INFO} ctxt
             (fn _ => Pretty.block [
-                Pretty.str "Failed to merge environment for smashed tpairs and environment created by flexflex_rule: ",
+                Pretty.str"Failed to merge environment for smashed tpairs and environment created by flexflex_rule: ",
                 pretty_unif_result ctxt (env, thm)
               ]|> Pretty.string_of);
             Seq.empty))
       end
     else Seq.single (env, thm)
   end
 
 fun abstract_abstract norm_term_type unify binders ctxt name T tbp =
   let
     val (binder as (_, bvar), ctxt') = Binders.fix_binder (name, T) ctxt
     fun norm_abstract (env, thm) =
       let fun norm_bvar env = norm_term_type (Envir.type_env env) bvar
       in
         smash_tpairs_if_occurs ctxt' (norm_bvar env) (env, thm)
         |> Seq.map_filter (fn (env, thm) =>
           UBase.abstract_rule ctxt' name (Thm.cterm_of ctxt' (norm_bvar env)) thm
           |> Option.map (pair env))
       end
   in unify (binder :: binders) ctxt' tbp #> Seq.maps norm_abstract end
 
 fun rigid_rigid norm_term_type unify_types ctxt s (nt, Tt) env =
   let val (ns, Ts) = (if is_Const s then dest_Const else dest_Free) s
   in
     if ns = nt then
       let val (env' as Envir.Envir {tyenv,...}) = unify_types ctxt (Ts, Tt) env
       in
         (env', UBase.reflexive_term ctxt (norm_term_type tyenv s))
         |> Seq.single
       end
     else Seq.empty
   end
 
 fun bound_bound binders ctxt (i, j) =
   if i = j
   then Binders.nth_binder_data binders i |> UBase.reflexive_term ctxt |> Seq.single
   else Seq.empty
 
 fun comb_comb norm_thm_types unify ctxt (f, x) (g, y) env =
   let
-    val unif' = unify ctxt
-    val env_thmq = unif' (f, g) env
-      |> Seq.maps (fn (env, thm_fg) => unif' (x, y) env |> Seq.map (apsnd (pair thm_fg)))
+    val unif = unify ctxt
+    val env_thmq = unif (f, g) env
+      |> Seq.maps (fn (env, thm_fg) => unif (x, y) env |> Seq.map (apsnd (pair thm_fg)))
     fun combine (env, thmp) =
       (*normalise types for the combination theorem to succeed*)
       apply2 (norm_thm_types ctxt env) thmp
       |> uncurry UBase.combination
       |> pair env
   in Seq.map combine env_thmq end
 
 fun args_args norm_thm_types unify ctxt (ss, ts) env_thmhq =
   (let
     val args = ss ~~ ts
     fun unif_arg tp = Seq.maps
       (fn (env, thms) => unify ctxt tp env |> Seq.map (apsnd (fn thm => thm :: thms)))
     fun unif_args env = fold unif_arg args (Seq.single (env, []))
     (*combine the theorems*)
     fun combine thmh (env_res, arg_thms) =
       let
         (*normalise types for the combination theorem to succeed*)
-        val norm_thm_types' = norm_thm_types ctxt env_res
-        fun norm_combine thm_arg thm = norm_thm_types' thm_arg |> UBase.combination thm
-      in (env_res, fold_rev norm_combine arg_thms (norm_thm_types' thmh)) end
+        val norm_thm_types = norm_thm_types ctxt env_res
+        fun norm_combine thm_arg thm = norm_thm_types thm_arg |> UBase.combination thm
+      in (env_res, fold_rev norm_combine arg_thms (norm_thm_types thmh)) end
   in Seq.maps (fn (env, thmh) => unif_args env |> Seq.map (combine thmh)) env_thmhq end)
   handle ListPair.UnequalLengths => Seq.empty
 
 fun strip_comb_strip_comb norm_thm_types unify binders ctxt (sh, th) (ss, ts) =
   unify binders ctxt (sh, th)
   #> args_args norm_thm_types (unify binders) ctxt (ss, ts)
 
 
 (* logging *)
 
 fun log_unif_result ctxt _ res =
   @{log Logger.INFO} ctxt (fn _ => pretty_unif_result ctxt res |> Pretty.string_of)
 
 fun log_unif_results ctxt tp unify =
   let val res = unify ctxt tp (empty_envir tp) |> Seq.list_of
   in fold (log_unif_result ctxt tp #> K) res () end
 
 fun log_unif_results' limit ctxt tp unify =
   let val res = unify ctxt tp (empty_envir tp) |> Seq.take limit |> Seq.list_of
   in fold (log_unif_result ctxt tp #> K) res () end
 
 end