--- a/src/HOL/Import/import_rule.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Dec 22 21:03:16 2023 +0100
@@ -172,9 +172,8 @@
val constbinding = Binding.name constname
val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
- val (thms, thy2) = Global_Theory.add_defs false
- [((Binding.suffix_name "_hldef" constbinding, eq), [])] thy1
- val def_thm = freezeT thy1 (hd thms)
+ val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" constbinding, eq) thy1
+ val def_thm = freezeT thy1 thm
in
(meta_eq_to_obj_eq def_thm, thy2)
end