diff -r 372ff330a9d9 -r d25181c1807a src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jan 21 00:01:31 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 15:48:39 2025 +0100
@@ -55,7 +55,7 @@
 
 (* basic logic *)
 
-fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
+fun implies_elim_all th = implies_elim_list th (map Thm.assume_cterm (cprems_of th))
 
 fun meta_mp th1 th2 =
   let
@@ -122,7 +122,7 @@
     val th1b = Thm.implies_intr th2c th1a
     val th2b = Thm.implies_intr th1c th2a
     val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
-    val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
+    val i1 = Thm.implies_elim i (Thm.assume_cterm (Thm.cprop_of th2b))
     val i2 = Thm.implies_elim i1 th1b
     val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
     val i4 = Thm.implies_elim i3 th2b