src/HOL/Decision_Procs/Reflective_Field.thy

     (term_of_pexpr y, HOLogic.mk_list \<^Type>\<open>pexpr\<close> (map term_of_pexpr zs)));
 
 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
   (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
 

         get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R;
       val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd);
       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 =
         Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv
           (binop_conv