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