# HG changeset patch
# User wenzelm
# Date 1686044018 -7200
# Node ID e1bd2eb4c407774cfb92a9c677034ef510d710a7
# Parent  db2a6f9aaa779daddf77f43c3238f94be29eb51b
tuned;

diff -r db2a6f9aaa77 -r e1bd2eb4c407 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jun 06 11:26:59 2023 +0200
+++ b/src/Pure/drule.ML	Tue Jun 06 11:33:38 2023 +0200
@@ -171,9 +171,8 @@
   -- reverses the effect of gen_all modulo higher-order unification*)
 fun lift_all ctxt raw_goal raw_th =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val goal = Thm.transfer_cterm thy raw_goal;
-    val th = Thm.transfer thy raw_th;
+    val goal = Thm.transfer_cterm' ctxt raw_goal;
+    val th = Thm.transfer' ctxt raw_th;
 
     val maxidx = Thm.maxidx_of th;
     val ps = outer_params (Thm.term_of goal)
@@ -686,10 +685,12 @@
 
 fun norm_hhf_cterm ctxt raw_ct =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val ct = Thm.transfer_cterm thy raw_ct;
+    val ct = Thm.transfer_cterm' ctxt raw_ct;
     val t = Thm.term_of ct;
-  in if is_norm_hhf {protect = false} t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
+  in
+    if is_norm_hhf {protect = false} t then ct
+    else Thm.cterm_of ctxt (norm_hhf (Proof_Context.theory_of ctxt) t)
+  end;
 
 
 (* var indexes *)
diff -r db2a6f9aaa77 -r e1bd2eb4c407 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jun 06 11:26:59 2023 +0200
+++ b/src/Pure/more_thm.ML	Tue Jun 06 11:33:38 2023 +0200
@@ -266,7 +266,7 @@
 
 fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
   let
-    val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
+    val ct = Thm.transfer_cterm' ctxt raw_ct;
     val hyps' = Termset.insert (Thm.term_of ct) hyps;
   in (checked_hyps, hyps', shyps) end);
 
diff -r db2a6f9aaa77 -r e1bd2eb4c407 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Jun 06 11:26:59 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Jun 06 11:33:38 2023 +0200
@@ -967,7 +967,6 @@
 
 fun rewritec (prover, maxt) ctxt t =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val Simpset ({rules, ...}, {congs, procs, term_ord, ...}) = simpset_of ctxt;
     val eta_thm = Thm.eta_conversion t;
     val eta_t' = Thm.rhs_of eta_thm;
@@ -975,8 +974,8 @@
     fun rew rrule =
       let
         val {thm = thm0, name, lhs, elhs = elhs0, extra, fo, perm} = rrule;
-        val thm = Thm.transfer thy thm0;
-        val elhs = Thm.transfer_cterm thy elhs0;
+        val thm = Thm.transfer' ctxt thm0;
+        val elhs = Thm.transfer_cterm' ctxt elhs0;
         val prop = Thm.prop_of thm;
         val (rthm, elhs') =
           if maxt = ~1 orelse not extra then (thm, elhs)
@@ -1343,10 +1342,8 @@
 
 fun rewrite_cterm mode prover raw_ctxt raw_ct =
   let
-    val thy = Proof_Context.theory_of raw_ctxt;
-
     val ct = raw_ct
-      |> Thm.transfer_cterm thy
+      |> Thm.transfer_cterm' raw_ctxt
       |> Thm.adjust_maxidx_cterm ~1;
     val maxidx = Thm.maxidx_of_cterm ct;