# HG changeset patch
# User haftmann
# Date 1534761893 0
# Node ID 8fbfb67f6824d1adb060ba47e04e8fe8f9bd61c3
# Parent  9fc50a3e07f6b140b4bf9f3151dc3ca44ab5bd7f
removed ineffective code declarations

diff -r 9fc50a3e07f6 -r 8fbfb67f6824 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/List.thy	Mon Aug 20 10:44:53 2018 +0000
@@ -2985,14 +2985,10 @@
   "INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
   using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
 
-declare INF_set_fold [code]
-
 lemma (in complete_lattice) SUP_set_fold:
   "SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
   using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
 
-declare SUP_set_fold [code]
-
 
 subsubsection \<open>Fold variants: @{const foldr} and @{const foldl}\<close>