diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 28 20:10:23 2021 +0200
@@ -21,10 +21,10 @@
   "Sup :: _ Predicate.pred set \<Rightarrow> _"
   pred_of_set
   Wellfounded.acc
-  Cardinality.card'
-  Cardinality.finite'
-  Cardinality.subset'
-  Cardinality.eq_set
+  Code_Cardinality.card'
+  Code_Cardinality.finite'
+  Code_Cardinality.subset'
+  Code_Cardinality.eq_set
   Euclidean_Algorithm.Gcd
   Euclidean_Algorithm.Lcm
   "Gcd :: _ poly set \<Rightarrow> _"