--- a/src/HOL/Library/Mapping.thy Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Jun 06 21:28:46 2016 +0200
@@ -121,7 +121,7 @@
definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
declare [[code drop: Mapping.lookup]]
-setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
+setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<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 .