diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 16:22:15 2025 +0100
@@ -339,8 +339,8 @@
       | NONE => Sign.full_bname thy (#isabelle (make_name c)))
   in Thm.global_cterm_of thy (Const (d, Thm.typ_of ty)) end
 
-val make_thm = Skip_Proof.make_thm_cterm o Thm.apply \<^cterm>\<open>Trueprop\<close>
-val assume_thm = Thm.trivial o Thm.apply \<^cterm>\<open>Trueprop\<close>
+val make_thm = Skip_Proof.make_thm_cterm o HOLogic.mk_judgment
+val assume_thm = Thm.trivial o HOLogic.mk_judgment
 
 
 (* import file *)