# HG changeset patch
# User haftmann
# Date 1434092003 -7200
# Node ID db9c67b760f1844dd753462a297443559658a2d0
# Parent  ce559c850a278e371fdaea2171b08e2abfd6331c
dropped warnings by dropping ineffective code declarations

diff -r ce559c850a27 -r db9c67b760f1 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -1478,7 +1478,7 @@
   by (induct rule: finite.induct[OF `finite A`])
     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
 
-lemma Lcm_set [code, code_unfold]:
+lemma Lcm_set [code_unfold]:
   "Lcm (set xs) = fold lcm xs 1"
   using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps)
 
@@ -1571,7 +1571,7 @@
   by (induct rule: finite.induct[OF `finite A`])
     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
 
-lemma Gcd_set [code, code_unfold]:
+lemma Gcd_set [code_unfold]:
   "Gcd (set xs) = fold gcd xs 0"
   using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)