diff -r d9df588f8910 -r bd3685e5f883 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jul 23 13:22:51 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jul 23 13:22:58 2025 +0200
@@ -17,10 +17,6 @@
 \<close>
 
 declare [[code drop:
-  "Inf :: _ Predicate.pred set \<Rightarrow> _"
-  "Sup :: _ Predicate.pred set \<Rightarrow> _"
-  pred_of_set
-  Wellfounded.acc
   Code_Cardinality.card'
   Code_Cardinality.finite'
   Code_Cardinality.subset'