diff -r 96ba073260ef -r b6e117b5d0f0 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Sep 11 09:06:49 2025 +0200
+++ b/src/Pure/Isar/code.ML	Thu Sep 11 10:47:25 2025 +0200
@@ -1509,15 +1509,26 @@
 val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
 val declare_abstract_eqn = code_declaration Liberal Morphism.thm generic_declare_abstract_eqn;
 
+fun declare_from_thm decl thm thy =
+  case prep_eqn Liberal thy (thm, false) of
+    SOME (c, _) => decl c thy
+  | NONE => thy;
+
 fun declare_aborting_global c =
   modify_specs (register_fun_spec c (Eqns []));
 
+val declare_aborting_global' =
+  declare_from_thm declare_aborting_global;
+
 fun declare_unimplemented_global c thy =
   if Config.get_global thy strict_drop
     andalso is_unimplemented (the_fun_spec (specs_of thy) c)
   then error "No implementation to drop"
   else modify_specs (register_fun_spec c Unimplemented) thy;
 
+val declare_unimplemented_global' =
+  declare_from_thm declare_unimplemented_global;
+
 
 (* cases *)
 
@@ -1591,11 +1602,15 @@
       || code_thm_attribute (Args.$$$ "abstype")
           (generic_declare_abstype Liberal)
       || code_thm_attribute Args.del
-          del_eqn_global
+          (fn thm => tap (fn _ => Output.legacy_feature "code del attribute") (del_eqn_global thm))
       || code_const_attribute (Args.$$$ "abort")
           declare_aborting_global
+      || code_thm_attribute (Args.$$$ "abort")
+          declare_aborting_global'
       || code_const_attribute (Args.$$$ "drop")
           declare_unimplemented_global
+      || code_thm_attribute (Args.$$$ "drop")
+          declare_unimplemented_global'
       || Scan.succeed (code_attribute
           add_maybe_abs_eqn_liberal);
   in