src/HOL/Library/Mapping.thy

 
 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
   morphisms rep Mapping
   ..
 
-setup_lifting (no_code) type_definition_mapping
+setup_lifting type_definition_mapping
 
 lift_definition empty :: "('a, 'b) mapping"
   is Map.empty parametric empty_parametric .
 
 lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option"
   is "\<lambda>m k. m k" parametric lookup_parametric .
 
+declare [[code drop: Mapping.lookup]]
+setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close>
+
 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 .
 
 lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   is "\<lambda>k m. m(k := None)" parametric delete_parametric .

 lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping"
   is "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_parametric .
 
 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping"
   is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric .
+
+declare [[code drop: map]]
 
 
 subsection {* Functorial structure *}
 
 functor map: map

 qed
 
 
 subsection {* Code generator setup *}
 
-code_datatype empty update
-
 hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
   replace default map_entry map_default tabulate bulkload map of_alist
 
 end
+