src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/HOL.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -1856,8 +1856,8 @@
   using assms by simp_all
 
 setup \<open>
-  Code.add_case @{thm Let_case_cert} #>
-  Code.add_undefined @{const_name undefined}
+  Code.declare_case_global @{thm Let_case_cert} #>
+  Code.declare_undefined_global @{const_name undefined}
 \<close>
 
 declare [[code abort: undefined]]