src/HOL/HOL.thy
changeset 66251 cd935b7cb3fb
parent 66109 e034a563ed7d
child 66836 4eb431c3f974
     1.1 --- a/src/HOL/HOL.thy	Mon Jul 03 14:25:07 2017 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jul 02 20:13:38 2017 +0200
     1.3 @@ -1856,8 +1856,8 @@
     1.4    using assms by simp_all
     1.5  
     1.6  setup \<open>
     1.7 -  Code.add_case @{thm Let_case_cert} #>
     1.8 -  Code.add_undefined @{const_name undefined}
     1.9 +  Code.declare_case_global @{thm Let_case_cert} #>
    1.10 +  Code.declare_undefined_global @{const_name undefined}
    1.11  \<close>
    1.12  
    1.13  declare [[code abort: undefined]]