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,155 +1,155 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>E-Unification Examples\<close>
 theory E_Unification_Examples
   imports
     Main
     ML_Unification_HOL_Setup
     Unify_Fact_Tactic
 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_first_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 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)
 
 lemma "(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[of s])
 
 subsection \<open>Providing Canonical Solutions With Unification Hints\<close>
 
-lemma [uhint]: "xs \<equiv> [] \<Longrightarrow> length xs \<equiv> 0" by simp
+lemma [uhint]: "length [] \<equiv> 0" by simp
 
 schematic_goal "length ?xs = 0"
   by (ufact refl)
 
-lemma [uhint]: "(n :: nat) \<equiv> m \<Longrightarrow> n - m \<equiv> 0" by simp
+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 fails because, by default, @{ML Standard_Unification_Hints.try_hints}
 uses the higher-order pattern unifier to unify hints against a given disagreement pair, and
 @{term 0} cannot be higher-order pattern unified with @{term "length []"}. The unification of the
 hint requires the use of yet another hint, namely @{term "length xs = 0"} (cf. above).\<close>
 schematic_goal "n - ?m = length []"
   \<comment> \<open>by (ufact refl)\<close>
   oops
 
 text \<open>There are two ways to fix this:
-\<^enum> We allow the recursive uses of unification hints when searching for suitable unification hints.
-\<^enum> We use a different unification hint that the recursive use of hints explicit.\<close>
+\<^enum> We allow the recursive use of unification hints when unifying @{thm sub_self_eq_zero} and our goal.
+\<^enum> We use a different unification hint that makes the recursive use of unification hints explicit.\<close>
 
-text \<open>Solution 1: recursive usages of hints. Warning: such recursive applications easily loop.\<close>
+text \<open>Solution 1: we can use @{attribute rec_uhint} for recursive usages of hints.
+Warning: recursive applications easily loop.\<close>
 schematic_goal "n - ?m = length []"
-  using [[uhint where concl_unifier = Standard_Mixed_Unification.first_higherp_first_comb_higher_unify]]
+  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 []"
   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,212 +1,213 @@
 \<^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
 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},
-but having separate instances is a cleaner approach.\<close>
+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),
-        prems_unifier = NONE,
-        concl_unifier = NONE,
         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)
     (Reification_Unification_Hints.try_hints
       |> Unification_Combinator.norm_unifier (#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 = Higher_Order_Pattern_Unification.match]]
 
 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> 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_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,32 +1,34 @@
 \<^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_first_comb_higher_unify)
   |> Unification_Combinator.unifier_from_closed_unifier
   |> K)
   (Standard_Unification_Combine.default_metadata \<^binding>\<open>SIMPS_TO_unif\<close>)\<close>]]
 
 declare [[ucombine add = \<open>Standard_Unification_Combine.eunif_data
   (Simplifier_Unification.SIMPS_TO_UNIF_unify @{thm eq_TrueI}
     Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify
     (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify
     |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif)
   |> Unification_Combinator.norm_unifier
     (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify)
   |> K)
   (Standard_Unification_Combine.default_metadata \<^binding>\<open>SIMPS_TO_UNIF_unif\<close>)\<close>]]
 
 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,55 +1,87 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>Unification Hints\<close>
 theory ML_Unification_Hints
   imports
     ML_Generic_Data_Utils
     ML_Term_Index
     ML_Unifiers
     ML_Unification_Parsers
 begin
 
 paragraph \<open>Summary\<close>
 text \<open>A generalisation of unification hints, originally introduced in \<^cite>\<open>"unif-hints"\<close>.
 We support a generalisation that
 \<^enum> allows additional universal variables in premises
 \<^enum> allows non-atomic left-hand sides for premises
 \<^enum> 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>
 \<close>
 
 ML_file\<open>unification_hints_base.ML\<close>
 ML_file\<open>unification_hints.ML\<close>
 ML_file\<open>term_index_unification_hints.ML\<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_first_comb_higher_unify,
+        prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify
+          |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
+        normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_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_first_comb_higher_unify}
+when looking for hints are accessible via @{attribute rec_uhint}.\<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 = SOME Higher_Ordern_Pattern_First_Decomp_Unification.unify,
-        normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify,
         prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify
           |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
+        normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_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>
 
-text\<open>Standard unification hints are accessible via @{attribute uhint}.\<close>
+text\<open>Standard unification hints using @{ML Higher_Ordern_Pattern_First_Decomp_Unification.unify}
+when looking for hints are accessible via @{attribute uhint}. Note: there will be no recursive
+usage of unification hints when searching for potential unification hints in this case. See also
+@{file "../Examples/E_Unification_Examples.thy"}\<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_first_comb_higher_unify)
+  |> K)
+  (Standard_Unification_Combine.default_metadata Standard_Unification_Hints_Rec.binding)\<close>]]
+and [[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_first_comb_higher_unify)
   |> K)
   (Standard_Unification_Combine.default_metadata Standard_Unification_Hints.binding)\<close>]]
 
+
 text\<open>Examples see @{dir "../Examples"}.\<close>
 
 end