# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID 8ff34c1ad580630a640b0101e5e21ee90c709c18
# Parent  567079abb17354d430ceab04dcc4554ffc5dc096
removed ineffective code equation

diff -r 567079abb173 -r 8ff34c1ad580 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Wed Aug 22 12:32:58 2018 +0000
+++ b/src/HOL/Library/Mapping.thy	Wed Aug 22 12:32:58 2018 +0000
@@ -117,10 +117,6 @@
 
 definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
 
-lemma [code abstract]:
-  "lookup (Mapping f) = f"
-  by (fact Mapping.lookup.abs_eq) (* FIXME lifting *)
-
 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .