diff -r f4613ca298e6 -r 7625b5d7cfe2 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 18:29:21 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 20:25:51 2021 +0200
@@ -660,7 +660,7 @@
 local
 
 fun pol (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 :: pol\<close>;
 
 val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result