src/HOL/Library/Fin_Fun.thy

--- a/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 18:26:12 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 21:13:47 2009 +0200
@@ -17,10 +17,6 @@
   For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
 *}
 
-(*FIXME move to Map.thy*)
-lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-  by (auto simp add: restrict_map_def intro: ext)
-
 
 subsection {* The @{text "map_default"} operation *}