--- 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 *)