diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Feb 26 18:33:01 2016 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Feb 26 22:15:09 2016 +0100
@@ -60,7 +60,19 @@
 
 lemma [code, code del]:
   "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
-  
+
+lemma [code, code del]:
+  "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
+
+lemma [code, code del]:
+  "(Lcm :: _ poly set \<Rightarrow> _) = Lcm" ..
+
+lemma [code, code del]:
+  "Gcd_eucl = Gcd_eucl" ..
+
+lemma [code, code del]:
+  "Lcm_eucl = Lcm_eucl" ..
+
 (*
   If the code generation ends with an exception with the following message:
   '"List.set" is not a constructor, on left hand side of equation: ...',