diff -r 58bf18aaf8ec -r 7eb451adbda6 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Aug 12 09:19:48 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Aug 12 08:56:25 2017 +0200
@@ -25,14 +25,8 @@
   Cardinality.finite'
   Cardinality.subset'
   Cardinality.eq_set
-  Gcd_fin
-  Lcm_fin
   Euclidean_Algorithm.Gcd
   Euclidean_Algorithm.Lcm
-  "Gcd :: nat set \<Rightarrow> nat"
-  "Lcm :: nat set \<Rightarrow> nat"
-  "Gcd :: int set \<Rightarrow> int"
-  "Lcm :: int set \<Rightarrow> int"
   "Gcd :: _ poly set \<Rightarrow> _"
   "Lcm :: _ poly set \<Rightarrow> _"
   permutations_of_set