# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1500558061 -7200
# Node ID f32968e099d5009e6d216629e6fbe250c5704fea
# Parent  2562f151541c0177c55462d48e0cd87aca1aa6ee
tuned code setup

diff -r 2562f151541c -r f32968e099d5 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Thu Jul 20 15:41:01 2017 +0200
@@ -1066,7 +1066,7 @@
 unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
 by (metis option.collapse option.rel_sel)
 
-lemmas fmap_generic_code =
+lemmas [code] =
   fmrel_code
   fmran'_alt_def
   fmdom'_alt_def
@@ -1114,8 +1114,6 @@
 
 end
 
-declare fmap_generic_code[code]
-
 
 subsection \<open>Instances\<close>