--- a/src/HOL/Decision_Procs/Reflective_Field.thy Sun Oct 24 18:29:21 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Sun Oct 24 20:25:51 2021 +0200
@@ -640,7 +640,7 @@
local
fun fnorm (ctxt, ct, t) =
- \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+ \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
@@ -881,7 +881,7 @@
val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
val ce = Thm.cterm_of ctxt (reif xs t);
val ce' = Thm.cterm_of ctxt (reif xs u);
- val fnorm = cv ctxt \<^let>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
+ val fnorm = cv ctxt \<^instantiate>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
val (_, [_, c]) = strip_app dc;
val th =