diff -r 766db3539859 -r fc9265882329 src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:20 2017 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 19:13:49 2017 +0100
@@ -981,12 +981,9 @@
   shows "lcm p q = normalize (p * q) div gcd p q"
   by (fact lcm_gcd)
 
-declare Gcd_set
-  [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
-declare Lcm_set
-  [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
+lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+  
 text \<open>Example:
   @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
 \<close>