# HG changeset patch
# User wenzelm
# Date 1684006234 -7200
# Node ID 9da707dad2a350b5901cda98ebd669fc068cc7a4
# Parent  2594319ad9eec33e6736cf87e7383364302a4ebb
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;

diff -r 2594319ad9ee -r 9da707dad2a3 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu May 11 22:12:43 2023 +0200
+++ b/src/Pure/simplifier.ML	Sat May 13 21:30:34 2023 +0200
@@ -161,15 +161,15 @@
 
 local
 
-fun make_cong ctxt = Thm.close_derivation \<^here> o Thm.reflexive
-  o Thm.cterm_of ctxt o Logic.varify_global o list_comb;
+fun make_cong thy = Thm.close_derivation \<^here> o Thm.reflexive
+  o Thm.global_cterm_of thy o Logic.varify_global o list_comb;
 
 fun add_cong (const_binding, (const, target_params)) gthy =
   if null target_params
   then gthy
   else
     let
-      val cong = make_cong (Context.proof_of gthy) (const, target_params)
+      val cong = make_cong (Context.theory_of gthy) (const, target_params)
       val cong_binding = Binding.qualify_name true const_binding "cong"
     in
       gthy