diff --git a/library/init/meta/decl_cmds.lean b/library/init/meta/decl_cmds.lean
index a177f8ac4a..5bc92825f2 100644
--- a/library/init/meta/decl_cmds.lean
+++ b/library/init/meta/decl_cmds.lean
@@ -36,17 +36,17 @@ e^.replace (λ e d,
    creates the declaration
         lemma g_lemma : forall a, g a > 0 := ... -/
 meta def copy_decl_updating_type (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
-do env       ← get_env,
-   decl      ← returnex $ env^.get src_decl_name,
-   new_type  ← return $ apply_replacement replacements decl^.type,
-   new_value ← return $ expr.const src_decl_name (decl^.univ_params^.for level.param),
-   add_decl (((decl^.to_definition^.update_type new_type)^.update_name new_decl_name)^.update_value new_value),
-   return ()
+do env  ← get_env,
+   decl ← returnex $ env^.get src_decl_name,
+   decl ← return $ decl^.update_name $ new_decl_name,
+   decl ← return $ decl^.update_type $ apply_replacement replacements decl^.type,
+   decl ← return $ decl^.update_value $ expr.const src_decl_name (decl^.univ_params^.for level.param),
+   add_decl decl
 
 meta def copy_decl_using (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
-do env       ← get_env,
-   decl      ← returnex $ env^.get src_decl_name,
-   new_type  ← return $ apply_replacement replacements decl^.type,
-   new_value ← return $ task.map (apply_replacement replacements) decl^.value_task,
-   add_decl (((decl^.to_definition^.update_type new_type)^.update_name new_decl_name)^.update_value_task new_value),
-   return ()
+do env  ← get_env,
+   decl ← returnex $ env^.get src_decl_name,
+   decl ← return $ decl^.update_name $ new_decl_name,
+   decl ← return $ decl^.update_type $ apply_replacement replacements decl^.type,
+   decl ← return $ decl^.map_value $ apply_replacement replacements,
+   add_decl decl
diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean
index 6930f5aeb5..be2bb4cba0 100644
--- a/library/init/meta/declaration.lean
+++ b/library/init/meta/declaration.lean
@@ -107,6 +107,11 @@ meta def declaration.update_value_task : declaration → task expr → declarati
 | (declaration.thm n ls t v)       new_v := declaration.thm n ls t new_v
 | d                                new_v := d
 
+meta def declaration.map_value : declaration → (expr → expr) → declaration
+| (declaration.defn n ls t v h tr) f := declaration.defn n ls t (f v) h tr
+| (declaration.thm n ls t v)       f := declaration.thm n ls t (task.map f v)
+| d                                f := d
+
 meta def declaration.to_definition : declaration → declaration
 | (declaration.cnst n ls t tr) := declaration.defn n ls t (default expr) reducibility_hints.abbrev tr
 | (declaration.ax n ls t)      := declaration.thm n ls t (task.pure (default expr))