# HG changeset patch
# User haftmann
# Date 1499019218 -7200
# Node ID cd935b7cb3fb2eea6bb1005f54e8629cb9c95a58
# Parent  56a87a5093be1b103a12043390df9c4b3125916b
proper concept of code declaration wrt. atomicity and Isar declarations

diff -r 56a87a5093be -r cd935b7cb3fb src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Doc/Codegen/Further.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -215,121 +215,4 @@
   short primer document.
 \<close>
 
-
-subsection \<open>ML system interfaces \label{sec:ml}\<close>
-
-text \<open>
-  Since the code generator framework not only aims to provide a nice
-  Isar interface but also to form a base for code-generation-based
-  applications, here a short description of the most fundamental ML
-  interfaces.
-\<close>
-
-subsubsection \<open>Managing executable content\<close>
-
-text %mlref \<open>
-  \begin{mldecls}
-  @{index_ML Code.read_const: "theory -> string -> string"} \\
-  @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\
-  @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
-  @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
-  @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
-  @{index_ML Code_Preproc.add_functrans: "
-    string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
-      -> theory -> theory"} \\
-  @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
-  @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
-  @{index_ML Code.get_type: "theory -> string
-    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
-  @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
-  \end{mldecls}
-
-  \begin{description}
-
-  \item @{ML Code.read_const}~@{text thy}~@{text s}
-     reads a constant as a concrete term expression @{text s}.
-
-  \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation
-     @{text "thm"} to executable content.
-
-  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation
-     @{text "thm"} from executable content, if present.
-
-  \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
-     the preprocessor simpset.
-
-  \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
-     function transformer @{text f} (named @{text name}) to executable content;
-     @{text f} is a transformer of the code equations belonging
-     to a certain function definition, depending on the
-     current theory context.  Returning @{text NONE} indicates that no
-     transformation took place;  otherwise, the whole process will be iterated
-     with the new code equations.
-
-  \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
-     function transformer named @{text name} from executable content.
-
-  \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
-     a datatype to executable content, with generation
-     set @{text cs}.
-
-  \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
-     returns type constructor corresponding to
-     constructor @{text const}; returns @{text NONE}
-     if @{text const} is no constructor.
-
-  \end{description}
-\<close>
-
-
-subsubsection \<open>Data depending on the theory's executable content\<close>
-
-text \<open>
-  Implementing code generator applications on top of the framework set
-  out so far usually not only involves using those primitive
-  interfaces but also storing code-dependent data and various other
-  things.
-
-  Due to incrementality of code generation, changes in the theory's
-  executable content have to be propagated in a certain fashion.
-  Additionally, such changes may occur not only during theory
-  extension but also during theory merge, which is a little bit nasty
-  from an implementation point of view.  The framework provides a
-  solution to this technical challenge by providing a functorial data
-  slot @{ML_functor Code_Data}; on instantiation of this functor, the
-  following types and operations are required:
-
-  \medskip
-  \begin{tabular}{l}
-  @{text "type T"} \\
-  @{text "val empty: T"} \\
-  \end{tabular}
-
-  \begin{description}
-
-  \item @{text T} the type of data to store.
-
-  \item @{text empty} initial (empty) data.
-
-  \end{description}
-
-  \noindent An instance of @{ML_functor Code_Data} provides the
-  following interface:
-
-  \medskip
-  \begin{tabular}{l}
-  @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
-  @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
-  \end{tabular}
-
-  \begin{description}
-
-  \item @{text change} update of current data (cached!) by giving a
-    continuation.
-
-  \item @{text change_yield} update with side result.
-
-  \end{description}
-\<close>
-
 end
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -25,7 +25,7 @@
   val tycos = Sign.logical_types thy;
   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts thy end
+in fold Code.declare_unimplemented_global consts thy end
 \<close>
 
 text \<open>Simple example for the predicate compiler.\<close>
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -18,4 +18,3 @@
 export_code _ checking SML OCaml? Haskell? Scala
 
 end
-
diff -r 56a87a5093be -r cd935b7cb3fb 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]]
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Library/Mapping.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -117,8 +117,9 @@
 
 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_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close>  (* FIXME lifting *)
+lemma [code abstract]:
+  "lookup (Mapping f) = f"
+  by (fact Mapping.lookup.abs_eq) (* FIXME lifting *)
 
 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 .
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -2834,7 +2834,7 @@
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add,
-        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
+        Named_Theorems.add @{named_theorems nitpick_simp}]
       else [];
     val ((simps' :: rules', [induct']), thy2) =
       Proof_Context.theory_of ctxt1
@@ -2842,7 +2842,8 @@
       |> Global_Theory.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
+      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules)
+      ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy3 =
       thy2
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Predicate.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -208,16 +208,14 @@
   by (auto simp add: is_empty_def)
 
 definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
-  "\<And>default. singleton default A = (if \<exists>!x. eval A x then THE x. eval A x else default ())"
+  "singleton default A = (if \<exists>!x. eval A x then THE x. eval A x else default ())" for default
 
 lemma singleton_eqI:
-  fixes default
-  shows "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton default A = x"
+  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton default A = x" for default
   by (auto simp add: singleton_def)
 
 lemma eval_singletonI:
-  fixes default
-  shows "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton default A)"
+  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton default A)" for default
 proof -
   assume assm: "\<exists>!x. eval A x"
   then obtain x where x: "eval A x" ..
@@ -226,8 +224,7 @@
 qed
 
 lemma single_singleton:
-  fixes default
-  shows "\<exists>!x. eval A x \<Longrightarrow> single (singleton default A) = A"
+  "\<exists>!x. eval A x \<Longrightarrow> single (singleton default A) = A" for default
 proof -
   assume assm: "\<exists>!x. eval A x"
   then have "eval A (singleton default A)"
@@ -242,23 +239,19 @@
 qed
 
 lemma singleton_undefinedI:
-  fixes default
-  shows "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()"
+  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()" for default
   by (simp add: singleton_def)
 
 lemma singleton_bot:
-  fixes default
-  shows "singleton default \<bottom> = default ()"
+  "singleton default \<bottom> = default ()" for default
   by (auto simp add: bot_pred_def intro: singleton_undefinedI)
 
 lemma singleton_single:
-  fixes default
-  shows "singleton default (single x) = x"
+  "singleton default (single x) = x" for default
   by (auto simp add: intro: singleton_eqI singleI elim: singleE)
 
 lemma singleton_sup_single_single:
-  fixes default
-  shows "singleton default (single x \<squnion> single y) = (if x = y then x else default ())"
+  "singleton default (single x \<squnion> single y) = (if x = y then x else default ())" for default
 proof (cases "x = y")
   case True then show ?thesis by (simp add: singleton_single)
 next
@@ -274,12 +267,10 @@
 qed
 
 lemma singleton_sup_aux:
-  fixes default
-  shows
   "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B
     else if B = \<bottom> then singleton default A
     else singleton default
-      (single (singleton default A) \<squnion> single (singleton default B)))"
+      (single (singleton default A) \<squnion> single (singleton default B)))" for default
 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
   case True then show ?thesis by (simp add: single_singleton)
 next
@@ -306,11 +297,9 @@
 qed
 
 lemma singleton_sup:
-  fixes default
-  shows
   "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B
     else if B = \<bottom> then singleton default A
-    else if singleton default A = singleton default B then singleton default A else default ())"
+    else if singleton default A = singleton default B then singleton default A else default ())" for default
   using singleton_sup_aux [of default A B] by (simp only: singleton_sup_single_single)
 
 
@@ -567,24 +556,21 @@
   by (simp add: null_is_empty Seq_def)
 
 primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
-  [code del]: "\<And>default. the_only default Empty = default ()"
-| "\<And>default. the_only default (Insert x P) =
-    (if is_empty P then x else let y = singleton default P in if x = y then x else default ())"
-| "\<And>default. the_only default (Join P xq) =
+  "the_only default Empty = default ()" for default
+| "the_only default (Insert x P) =
+    (if is_empty P then x else let y = singleton default P in if x = y then x else default ())" for default
+| "the_only default (Join P xq) =
     (if is_empty P then the_only default xq else if null xq then singleton default P
        else let x = singleton default P; y = the_only default xq in
-       if x = y then x else default ())"
+       if x = y then x else default ())" for default
 
 lemma the_only_singleton:
-  fixes default
-  shows "the_only default xq = singleton default (pred_of_seq xq)"
+  "the_only default xq = singleton default (pred_of_seq xq)" for default
   by (induct xq)
     (auto simp add: singleton_bot singleton_single is_empty_def
     null_is_empty Let_def singleton_sup)
 
 lemma singleton_code [code]:
-  fixes default
-  shows
   "singleton default (Seq f) =
     (case f () of
       Empty \<Rightarrow> default ()
@@ -594,7 +580,7 @@
     | Join P xq \<Rightarrow> if is_empty P then the_only default xq
         else if null xq then singleton default P
         else let x = singleton default P; y = the_only default xq in
-          if x = y then x else default ())"
+          if x = y then x else default ())" for default
   by (cases "f ()")
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -49,7 +49,7 @@
   shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
   using assms by simp_all
 
-setup \<open>Code.add_case @{thm If_case_cert}\<close>
+setup \<open>Code.declare_case_global @{thm If_case_cert}\<close>
 
 code_printing
   constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/String.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -319,7 +319,7 @@
 definition implode :: "string \<Rightarrow> String.literal"
 where
   [code del]: "implode = STR"
-  
+
 instantiation literal :: size
 begin
 
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -1386,11 +1386,8 @@
             |> Proof_Context.export names_lthy lthy
           end;
 
-        val code_attrs =
-          if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
         val anonymous_notes =
-          [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
+          [(rel_code_thms, nitpicksimp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
         val notes =
@@ -1402,7 +1399,7 @@
            (ctr_transferN, ctr_transfer_thms, K []),
            (disc_transferN, disc_transfer_thms, K []),
            (sel_transferN, sel_transfer_thms, K []),
-           (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
+           (mapN, map_thms, K (nitpicksimp_attrs @ simp_attrs)),
            (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
            (map_selN, map_sel_thms, K []),
            (pred_injectN, pred_injects, K simp_attrs),
@@ -1411,7 +1408,7 @@
            (rel_injectN, rel_inject_thms, K simp_attrs),
            (rel_introsN, rel_intro_thms, K []),
            (rel_selN, rel_sel_thms, K []),
-           (setN, set_thms, K (code_attrs @ case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
+           (setN, set_thms, K (case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
            (set_casesN, set_cases_thms, nth set_cases_attrss),
            (set_introsN, set_intros_thms, K []),
            (set_selN, set_sel_thms, K [])]
@@ -1422,6 +1419,7 @@
           |> fp = Least_FP
             ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
           |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
+          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
           |> Local_Theory.notes (anonymous_notes @ notes);
 
         val subst = Morphism.thm (substitute_noted_thm noted);
@@ -1848,11 +1846,9 @@
 
     val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
 
-    val code_attrs =
-      if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
   in
     ((induct_thms, induct_thm, mk_induct_attrs ctrss),
-     (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
+     (rec_thmss, nitpicksimp_attrs @ simp_attrs))
   end;
 
 fun mk_coinduct_attrs fpTs ctrss discss mss =
@@ -2480,9 +2476,6 @@
     val fpTs = map (domain_type o fastype_of) dtors;
     val fpBTs = map B_ify_T fpTs;
 
-    val code_attrs =
-      if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
     val real_unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fpTs);
 
     val ctr_Tsss = map (map (map real_unfreeze_fp)) ctrXs_Tsss;
@@ -2698,6 +2691,7 @@
       in
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
+        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
         |> Local_Theory.notes (common_notes @ notes)
         (* for "datatype_realizer.ML": *)
         |>> name_noted_thms
@@ -2865,7 +2859,7 @@
             fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
            (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
            (corecN, corec_thmss, K []),
-           (corec_codeN, map single corec_code_thms, K (code_attrs @ nitpicksimp_attrs)),
+           (corec_codeN, map single corec_code_thms, K (nitpicksimp_attrs)),
            (corec_discN, corec_disc_thmss, K []),
            (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
            (corec_selN, corec_sel_thmss, K corec_sel_attrs),
@@ -2878,6 +2872,7 @@
         lthy
         |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
           [flat corec_sel_thmss, flat corec_thmss]
+        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
         |> Local_Theory.notes (common_notes @ notes)
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -2121,8 +2121,6 @@
           |> derive_and_update_coinduct_cong_intross [corec_info];
         val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
         val anonymous_notes = [];
 (* TODO:
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
@@ -2131,7 +2129,7 @@
 
         val notes =
           [(cong_introsN, maps snd cong_intros_pairs, []),
-           (codeN, [code_thm], code_attrs @ nitpicksimp_attrs),
+           (codeN, [code_thm], nitpicksimp_attrs),
            (coinductN, [coinduct], coinduct_attrs),
            (inner_inductN, inner_fp_inducts, []),
            (uniqueN, uniques, [])] @
@@ -2160,6 +2158,7 @@
         |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat ctr_thmss)
 *)
         |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], [code_thm])
+        |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
       end;
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -1498,8 +1498,6 @@
         val common_name = mk_common_name fun_names;
         val common_qualify = fold_rev I qualifys;
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
         val anonymous_notes =
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
@@ -1516,7 +1514,7 @@
           [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
            (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms,
             coinduct_attrs),
-           (codeN, code_thmss, code_attrs @ nitpicksimp_attrs),
+           (codeN, code_thmss, nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),
@@ -1537,6 +1535,7 @@
         |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat ctr_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat code_thmss)
+        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd
         |> (fn lthy =>
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -460,16 +460,16 @@
   Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
   #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
 
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]};
+val nitpicksimp_simp_attrs = @{attributes [nitpick_simp, simp]};
 
 fun datatype_compat fpT_names lthy =
   let
     val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
       mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy;
 
-    val all_notes =
+    val (all_notes, rec_thmss) =
       (case lfp_sugar_thms of
-        NONE => []
+        NONE => ([], [])
       | SOME ((inducts, induct, induct_attrs), (rec_thmss, _)) =>
         let
           val common_name = compat_N ^ mk_common_name b_names;
@@ -482,7 +482,7 @@
 
           val notes =
             [(inductN, map single inducts, induct_attrs),
-             (recN, rec_thmss, code_nitpicksimp_simp_attrs)]
+             (recN, rec_thmss, nitpicksimp_simp_attrs)]
             |> filter_out (null o #2)
             |> maps (fn (thmN, thmss, attrs) =>
               if forall null thmss then
@@ -492,7 +492,7 @@
                     ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
                   compat_b_names thmss);
         in
-          common_notes @ notes
+          (common_notes @ notes, rec_thmss)
         end);
 
     val register_interpret =
@@ -503,6 +503,7 @@
     |> Local_Theory.raw_theory register_interpret
     |> Local_Theory.notes all_notes
     |> snd
+    |> Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
   end;
 
 val datatype_compat_global = Named_Target.theory_map o datatype_compat;
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -623,8 +623,6 @@
     val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
     val transfer = exists (can (fn Transfer_Option => ())) opts;
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
@@ -633,7 +631,7 @@
           val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
             @{map 3} (fn b => fn attrs => fn thm =>
-                ((Binding.qualify false prefix b, code_attrs @ nitpicksimp_simp_attrs @ attrs),
+                ((Binding.qualify false prefix b, nitpicksimp_simp_attrs @ attrs),
                  [([thm], [])]))
               bs attrss thms;
         in
@@ -645,7 +643,9 @@
     |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names qualifys simpss)
-      #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
+      #-> (fn notes =>
+        plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
+        #> pair (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>
     old_primrec int raw_fixes raw_specs lthy
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -355,9 +355,6 @@
             size_gen_o_map_thmss
           end;
 
-      (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
-      val code_attrs = Code.add_default_eqn_attrib Code.Equation;
-
       val massage_multi_notes =
         maps (fn (thmN, thmss, attrs) =>
           map2 (fn T_name => fn thms =>
@@ -367,7 +364,7 @@
         #> filter_out (null o fst o hd o snd);
 
       val notes =
-        [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+        [(sizeN, size_thmss, nitpicksimp_attrs @ simp_attrs),
          (size_genN, size_gen_thmss, []),
          (size_gen_o_mapN, size_gen_o_map_thmss, []),
          (size_neqN, size_neq_thmss, [])]
@@ -377,6 +374,8 @@
         lthy2
         |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
         |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
+        |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
+          (*Ideally, this would only be issued if the "code" plugin is enabled.*)
         |> Local_Theory.notes notes;
 
       val phi0 = substitute_noted_thm noted;
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -1072,19 +1072,17 @@
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
         val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
         val nontriv_disc_eq_thmss =
           map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
             handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
 
         val anonymous_notes =
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
-           (flat nontriv_disc_eq_thmss, code_attrs @ nitpicksimp_attrs)]
+           (flat nontriv_disc_eq_thmss, nitpicksimp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
         val notes =
-          [(caseN, case_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
+          [(caseN, case_thms, nitpicksimp_attrs @ simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
            (case_distribN, [case_distrib_thm], []),
@@ -1101,7 +1099,7 @@
            (expandN, expand_thms, []),
            (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
            (nchotomyN, [nchotomy_thm], []),
-           (selN, all_sel_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
+           (selN, all_sel_thms, nitpicksimp_attrs @ simp_attrs),
            (splitN, [split_thm], []),
            (split_asmN, [split_asm_thm], []),
            (split_selN, split_sel_thms, []),
@@ -1121,15 +1119,14 @@
           |> Local_Theory.declaration {syntax = false, pervasive = true}
             (fn phi => Case_Translation.register
                (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-          |> Local_Theory.background_theory
-            (fold (fold Code.del_eqn_silent) [nontriv_disc_defs, sel_defs])
           |> plugins code_plugin ?
-             Local_Theory.declaration {syntax = false, pervasive = false}
+             (Code.declare_default_eqns (map (rpair true) (flat nontriv_disc_eq_thmss @ case_thms @ all_sel_thms))
+             #> Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => Context.mapping
                   (add_ctr_code fcT_name (map (Morphism.typ phi) As)
                      (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
                      (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
-                  I)
+                  I))
           |> Local_Theory.notes (anonymous_notes @ notes)
           (* for "datatype_realizer.ML": *)
           |>> name_noted_thms fcT_name exhaustN;
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -109,12 +109,13 @@
     Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
     #> add_def
     #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
-    #-> fold Code.del_eqn
+    #> snd
     #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
     #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK
-      [((qualify reflN, [Code.add_default_eqn_attribute Code.Nbe]), [([thm], [])]),
-        ((qualify simpsN, [Code.add_default_eqn_attribute Code.Equation]), [(rev thms, [])])])
-    #> snd
+          [((qualify reflN, []), [([thm], [])]),
+            ((qualify simpsN, []), [(rev thms, [])])])
+    #-> (fn [(_, [thm]), (_, thms)] =>
+          Code.declare_default_eqns_global ((thm, false) :: map (rpair true) thms))
   end;
 
 fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
@@ -126,9 +127,9 @@
   in
     if can (Code.constrset_of_consts thy) unover_ctrs then
       thy
-      |> Code.add_datatype ctrs
-      |> fold_rev (Code.add_eqn (Code.Equation, true)) case_thms
-      |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms)
+      |> Code.declare_datatype_global ctrs
+      |> Code.declare_default_eqns_global (map (rpair true) (rev case_thms))
+      |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms)
       |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
         ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
     else
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -45,7 +45,7 @@
 open Function_Common
 
 val simp_attribs =
-  @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation]
+  @{attributes [simp, nitpick_simp]}
 
 val psimp_attribs =
   @{attributes [nitpick_psimp]}
@@ -195,6 +195,7 @@
       in
         lthy
         |> add_simps I "simps" I simp_attribs tsimps
+        ||> Code.declare_default_eqns (map (rpair true) tsimps)
         ||>> Local_Theory.note
           ((derived_name defname "induct", [Attrib.case_names case_names]), tinduct)
         ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -451,17 +451,17 @@
 
   in
     if is_valid_eq abs_eq_thm then
-      (ABS_EQ, Code.add_eqn (Code.Equation, true) abs_eq_thm thy)
+      (ABS_EQ, Code.declare_default_eqns_global [(abs_eq_thm, true)] thy)
     else
       let
         val (rty_body, qty_body) = get_body_types (rty, qty)
       in
         if rty_body = qty_body then
-          (REP_EQ, Code.add_eqn (Code.Equation, true) (the opt_rep_eq_thm) thy)
+          (REP_EQ, Code.declare_default_eqns_global [(the opt_rep_eq_thm, true)] thy)
         else
           if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
           then
-            (REP_EQ, Code.add_eqn (Code.Abstract, true) (the opt_rep_eq_thm) thy)
+            (REP_EQ, Code.declare_abstract_eqn_global (the opt_rep_eq_thm) thy)
           else
             (NONE_EQ, thy)
       end
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -177,25 +177,16 @@
       let
         val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
       in  
-         Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
+         Local_Theory.background_theory
+           (Code.declare_datatype_global [dest_Const fixed_abs]) lthy'
       end
     else
       lthy
   end
 
-fun define_abs_type quot_thm lthy =
-  if Lifting_Def.can_generate_code_cert quot_thm then
-    let
-      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
-      val add_abstype_attribute = 
-          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
-        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
-    in
-      lthy
-        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
-    end
-  else
-    lthy
+fun define_abs_type quot_thm =
+  Lifting_Def.can_generate_code_cert quot_thm ?
+    Code.declare_abstype (quot_thm RS @{thm Quotient_abs_rep});
 
 local
   exception QUOT_ERROR of Pretty.T list
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -276,7 +276,7 @@
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
-      (Binding.qualify false prefix b, Code.add_default_eqn_attrib Code.Equation :: attrs)) spec;
+      (Binding.qualify false prefix b, attrs)) spec;
     fun simp_attr_binding prefix =
       (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   in
@@ -286,7 +286,9 @@
       Spec_Rules.add Spec_Rules.Equational (ts, simps)
       #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
-      #>> (fn (_, simps'') => (ts, simps''))))
+      #-> (fn (_, simps'') => 
+        Code.declare_default_eqns (map (rpair true) simps'')
+        #> pair (ts, simps''))))
   end;
 
 in
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -570,7 +570,6 @@
         ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
         ((Binding.empty, [Simplifier.simp_add]),
           [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
-        ((Binding.empty, [Code.add_default_eqn_attribute Code.Equation]), [(rec_rewrites, [])]),
         ((Binding.empty, [iff_add]), [(flat inject, [])]),
         ((Binding.empty, [Classical.safe_elim NONE]),
           [(map (fn th => th RS notE) (flat distinct), [])]),
@@ -578,6 +577,7 @@
         ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
           named_rules @ unnamed_rules)
     |> snd
+    |> Code.declare_default_eqns_global (map (rpair true) rec_rewrites)
     |> Old_Datatype_Data.register dt_infos
     |> Context.theory_map (fold2 Case_Translation.register case_combs constrss)
     |> Old_Datatype_Data.interpretation_data (config, dt_names)
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Old_Datatype/old_size.ML
--- a/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -195,14 +195,15 @@
         val ([(_, size_thms)], thy'') = thy'
           |> Global_Theory.note_thmss ""
             [((Binding.name "size",
-                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
-                 Code.add_default_eqn_attribute Code.Equation]),
+                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}]),
               [(size_eqns, [])])];
 
       in
-        fold2 (fn new_type_name => fn size_name =>
+        thy''
+        |> fold2 (fn new_type_name => fn size_name =>
             BNF_LFP_Size.register_size_global new_type_name size_name refl(*dummy*) size_thms [])
-          new_type_names size_names thy''
+          new_type_names size_names 
+        |> Code.declare_default_eqns_global (map (rpair true) size_thms)
       end
   end;
 
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -1421,15 +1421,13 @@
     val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
       (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
-    val attrib = Thm.declaration_attribute (fn thm => Context.mapping
-      (Code.add_eqn (Code.Equation, false) thm) I)
-      (*FIXME default code equation!?*)
-    val thy''' =
-      cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
-      fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
-      [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
-        [attrib])] thy))
-      result_thms' thy'')
+    val thy''' = cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...."
+      (fn _ =>
+        thy''
+        |> fold_map (fn (name, result_thms) => (Global_Theory.add_thmss
+            [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [])]))
+            result_thms'
+        |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) (flat (flat (notes))))))
   in
     thy'''
   end
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -110,8 +110,7 @@
     val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
   in
     thy
-    |> Code.del_eqns const
-    |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*)
+    |> Code.declare_default_eqns_global (map (rpair true) eqs)
   end
 
 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -382,11 +382,11 @@
         val eqs = map (fn eq => Goal.prove lthy argnames [] eq
           (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))) eqs_t
       in
-        fold (fn (name, eq) => Local_Theory.note
-          ((Binding.qualify true prfx
-              (Binding.qualify true name (Binding.name "simps")),
-             [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd)
-          (names ~~ eqs) lthy
+        lthy
+        |> fold_map (fn (name, eq) => Local_Theory.note
+             (((Binding.qualify true prfx o Binding.qualify true name) (Binding.name "simps"), []), [eq]))
+               (names ~~ eqs) 
+        |-> (fn notes => Code.declare_default_eqns (map (rpair true) (maps snd notes)))
       end)
 
 
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -179,8 +179,8 @@
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> prove_simps
     |-> (fn simps => Local_Theory.note
-      ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
-    |> snd
+          ((b, @{attributes [simp, nitpick_simp]}), simps))
+    |-> (fn (_, thms) => Code.declare_default_eqns (map (rpair true) thms))
   end
 
 
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -83,8 +83,7 @@
     val eqs = map (mk_term_of_eq thy ty) cs;
  in
     thy
-    |> Code.del_eqns const
-    |> fold (Code.add_eqn (Code.Equation, false)) eqs
+    |> Code.declare_default_eqns_global (map (rpair true) eqs)
   end;
 
 fun ensure_term_of_code (tyco, (vs, cs)) =
@@ -115,8 +114,7 @@
     val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
  in
     thy
-    |> Code.del_eqns const
-    |> Code.add_eqn (Code.Equation, false) eq
+    |> Code.declare_default_eqns_global [(eq, true)]
   end;
 
 fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =
diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/record.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -1775,20 +1775,24 @@
       val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
       val ensure_exhaustive_record =
         ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
+      fun add_code eq_def thy =
+        let
+          val ctxt = Proof_Context.init_global thy;
+        in
+          thy
+          |> Code.declare_default_eqns_global
+               [(mk_eq (Proof_Context.init_global thy) eq_def, true), (mk_eq_refl (Proof_Context.init_global thy), false)]
+        end;
     in
       thy
-      |> Code.add_datatype [ext]
-      |> fold (Code.add_eqn (Code.Equation, true)) simps
+      |> Code.declare_datatype_global [ext]
+      |> Code.declare_default_eqns_global (map (rpair true) simps)
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
       |-> (fn (_, (_, eq_def)) =>
          Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
-      |-> (fn eq_def => fn thy =>
-            thy
-            |> Code.del_eqn eq_def
-            |> Code.add_eqn (Code.Equation, true) (mk_eq (Proof_Context.init_global thy) eq_def))
-      |> (fn thy => Code.add_eqn (Code.Nbe, true) (mk_eq_refl (Proof_Context.init_global thy)) thy)
+      |-> add_code
       |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
       |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
     end
@@ -2045,8 +2049,7 @@
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
-                map (rpair [Code.add_default_eqn_attribute Code.Equation]
-                o apfst (Binding.concealed o Binding.name)))
+                map (Thm.no_attributes o apfst (Binding.concealed o Binding.name)))
             [make_spec, fields_spec, extend_spec, truncate_spec]);
     val defs_ctxt = Proof_Context.init_global defs_thy;
 
@@ -2212,6 +2215,7 @@
           (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
           (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
           (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
+      |> Code.declare_default_eqns_global (map (rpair true) derived_defs)
       |> Global_Theory.note_thmss ""
        [((Binding.name "select_convs", []), [(sel_convs, [])]),
         ((Binding.name "update_convs", []), [(upd_convs, [])]),
diff -r 56a87a5093be -r cd935b7cb3fb src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Pure/Isar/code.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -30,29 +30,28 @@
   val pretty_cert: theory -> cert -> Pretty.T list
 
   (*executable code*)
-  val add_datatype: (string * typ) list -> theory -> theory
-  val add_datatype_cmd: string list -> theory -> theory
+  val declare_datatype_global: (string * typ) list -> theory -> theory
+  val declare_datatype_cmd: string list -> theory -> theory
   val datatype_interpretation:
     (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
       -> theory -> theory) -> theory -> theory
-  val add_abstype: thm -> theory -> theory
-  val add_abstype_default: thm -> theory -> theory
+  val declare_abstype: thm -> local_theory -> local_theory
+  val declare_abstype_global: thm -> theory -> theory
   val abstype_interpretation:
     (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
-  type kind
-  val Equation: kind
-  val Nbe: kind
-  val Abstract: kind
-  val add_eqn: kind * bool -> thm -> theory -> theory
-  val add_default_eqn_attribute: kind -> attribute
-  val add_default_eqn_attrib: kind -> Token.src
-  val del_eqn_silent: thm -> theory -> theory
-  val del_eqn: thm -> theory -> theory
-  val del_eqns: string -> theory -> theory
-  val del_exception: string -> theory -> theory
-  val add_case: thm -> theory -> theory
-  val add_undefined: string -> theory -> theory
+  val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory
+  val declare_default_eqns_global: (thm * bool) list -> theory -> theory
+  val declare_eqns: (thm * bool) list -> local_theory -> local_theory
+  val declare_eqns_global: (thm * bool) list -> theory -> theory
+  val add_eqn_global: thm * bool -> theory -> theory
+  val del_eqn_global: thm -> theory -> theory
+  val declare_abstract_eqn: thm -> local_theory -> local_theory
+  val declare_abstract_eqn_global: thm -> theory -> theory
+  val declare_empty_global: string -> theory -> theory
+  val declare_unimplemented_global: string -> theory -> theory
+  val declare_case_global: thm -> theory -> theory
+  val declare_undefined_global: string -> theory -> theory
   val get_type: theory -> string
     -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
   val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
@@ -169,21 +168,17 @@
 (* functions *)
 
 datatype fun_spec = Unimplemented
-  | Eqns_Default of (thm * bool) list * (thm * bool) list lazy
-      (* (cache for default equations, lazy computation of default equations)
-         -- helps to restore natural order of default equations *)
+  | Eqns_Default of (thm * bool) list
   | Eqns of (thm * bool) list
-  | Proj of (term * string) * bool
-  | Abstr of (thm * string) * bool;
+  | Proj of term * string
+  | Abstr of thm * string;
 
-val default_fun_spec = Eqns_Default ([], Lazy.value []);
+val default_fun_spec = Eqns_Default [];
 
 fun is_default (Eqns_Default _) = true
-  | is_default (Proj (_, default)) = default
-  | is_default (Abstr (_, default)) = default
   | is_default _ = false;
 
-fun associated_abstype (Abstr ((_, tyco), _)) = SOME tyco
+fun associated_abstype (Abstr (_, tyco)) = SOME tyco
   | associated_abstype _ = NONE;
 
 
@@ -648,6 +643,33 @@
 fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
 
 
+(* preparation and classification of code equations *)
+
+fun prep_eqn strictness thy =
+  apfst (meta_rewrite thy)
+  #> generic_assert_eqn strictness thy false
+  #> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn));
+  
+fun prep_eqns strictness thy =
+  map_filter (prep_eqn strictness thy)
+  #> AList.group (op =);
+
+fun prep_abs_eqn strictness thy =
+  meta_rewrite thy
+  #> generic_assert_abs_eqn strictness thy NONE
+  #> Option.map (fn abs_eqn => (const_abs_eqn thy (fst abs_eqn), abs_eqn));
+
+fun prep_maybe_abs_eqn thy raw_thm =
+  let
+    val thm = meta_rewrite thy raw_thm;
+    val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm;
+  in case some_abs_thm of
+      SOME (thm, tyco) => SOME (const_abs_eqn thy thm, ((thm, true), SOME tyco))
+    | NONE => generic_assert_eqn Liberal thy false (thm, false)
+        |> Option.map (fn (thm, _) => (const_eqn thy thm, ((thm, is_linear thm), NONE)))
+  end;
+
+
 (* abstype certificates *)
 
 local
@@ -947,12 +969,12 @@
 fun get_cert ctxt functrans c =
   case retrieve_raw (Proof_Context.theory_of ctxt) c of
     Unimplemented => nothing_cert ctxt c
-  | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
+  | Eqns_Default eqns => eqns
       |> cert_of_eqns_preprocess ctxt functrans c
   | Eqns eqns => eqns
       |> cert_of_eqns_preprocess ctxt functrans c
-  | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
-  | Abstr ((abs_thm, tyco), _) => abs_thm
+  | Proj (_, tyco) => cert_of_proj ctxt c tyco
+  | Abstr (abs_thm, tyco) => abs_thm
      |> preprocess Conv.arg_conv ctxt
      |> cert_of_abs ctxt tyco c;
 
@@ -1027,13 +1049,13 @@
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks)
         (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
-    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
-          pretty_equations const (map fst (Lazy.force eqns_lazy))
+    fun pretty_function (const, Eqns_Default eqns) =
+          pretty_equations const (map fst eqns)
       | pretty_function (const, Eqns eqns) =
           pretty_equations const (map fst eqns)
-      | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
+      | pretty_function (const, Proj (proj, _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
-      | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
+      | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
     fun pretty_typ (tyco, vs) = Pretty.str
       (string_of_typ thy (Type (tyco, map TFree vs)));
     fun pretty_typspec (typ, (cos, abstract)) = if null cos
@@ -1089,118 +1111,114 @@
 (* code equations *)
 
 (*
-  external distinction:
-    kind * default
-  processual distinction:
-    thm * proper  for concrete equations
-    thm  for abstract equations
-
   strictness wrt. shape of theorem propositions:
-    * default attributes: silent
-    * user attributes: warnings (after morphism application!)
-    * Isabelle/ML functions: strict
+    * default equations: silent
+    * using declarations and attributes: warnings (after morphism application!)
+    * using global declarations (... -> thy -> thy): strict
     * internal processing after storage: strict
 *)
 
-fun gen_add_eqn default (raw_thm, proper) thy =
-  let
-    val thm = Thm.close_derivation raw_thm;
-    val c = const_eqn thy thm;
-    fun update_subsume verbose (thm, proper) eqns =
-      let
-        val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
-          o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
-        val args = args_of thm;
-        val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
-        fun matches_args args' =
-          let
-            val k = length args' - length args
-          in if k >= 0
-            then Pattern.matchess thy (args, (map incr_idx o drop k) args')
-            else false
-          end;
-        fun drop (thm', proper') = if (proper orelse not proper')
-          andalso matches_args (args_of thm') then
-            (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
-                Thm.string_of_thm_global thy thm') else (); true)
-          else false;
-      in (thm, proper) :: filter_out drop eqns end;
-    fun natural_order eqns =
-      (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns []))
-    fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
-      | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
-          (*this restores the natural order and drops syntactic redundancies*)
-      | add_eqn' true fun_spec = fun_spec
-      | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
-      | add_eqn' false _ = Eqns [(thm, proper)];
-  in change_fun_spec c (add_eqn' default) thy end;
+fun generic_code_declaration strictness lift_phi f x =
+  Local_Theory.declaration
+    {syntax = false, pervasive = false}
+    (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
 
-fun gen_add_abs_eqn default raw_thm thy =
+fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi;
+fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi;
+
+local
+
+fun subsumptive_add thy verbose (thm, proper) eqns =
   let
-    val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm;
-    val c = const_abs_eqn thy abs_thm;
-  in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end;
-
-datatype kind = Equation | Nbe | Abstract;
+    val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
+      o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
+    val args = args_of thm;
+    val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
+    fun matches_args args' =
+      let
+        val k = length args' - length args
+      in if k >= 0
+        then Pattern.matchess thy (args, (map incr_idx o drop k) args')
+        else false
+      end;
+    fun drop (thm', proper') = if (proper orelse not proper')
+      andalso matches_args (args_of thm') then
+        (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
+            Thm.string_of_thm_global thy thm') else (); true)
+      else false;
+  in (thm, proper) :: filter_out drop eqns end;
 
-fun mk_eqn strictness thy = generic_assert_eqn strictness thy false o
-  apfst (meta_rewrite thy);
-
-fun mk_abs_eqn strictness thy = generic_assert_abs_eqn strictness thy NONE o
-  meta_rewrite thy;
-
-fun mk_maybe_abs_eqn thy raw_thm =
+fun add_eqn_for (c, proto_eqn) thy =
   let
-    val thm = meta_rewrite thy raw_thm;
-    val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm;
-  in case some_abs_thm
-   of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
-    | NONE => Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
-        (generic_assert_eqn Liberal thy false (thm, false))
-  end;
+    val eqn = apfst Thm.close_derivation proto_eqn;
+    fun add (Eqns eqns) = Eqns (subsumptive_add thy true eqn eqns)
+      | add _ = Eqns [eqn];
+  in change_fun_spec c add thy end;
+
+fun add_eqns_for default (c, proto_eqns) thy =
+  let
+    val eqns = []
+      |> fold_rev (subsumptive_add thy (not default)) proto_eqns
+      |> (map o apfst) Thm.close_derivation;
+    fun add (Eqns_Default _) = Eqns_Default eqns
+      | add data = data;
+  in change_fun_spec c (if default then add else K (Eqns eqns)) thy end;
 
-fun generic_add_eqn strictness (kind, default) thm thy =
-  case kind of
-    Equation => fold (gen_add_eqn default)
-      (the_list (mk_eqn strictness thy (thm, true))) thy
-  | Nbe => fold (gen_add_eqn default)
-      (the_list (mk_eqn strictness thy (thm, false))) thy
-  | Abstract => fold (gen_add_abs_eqn default)
-      (the_list (mk_abs_eqn strictness thy thm)) thy;
+fun add_abstract_for (c, proto_abs_eqn) =
+  let
+    val abs_eqn = apfst Thm.close_derivation proto_abs_eqn;
+  in change_fun_spec c (K (Abstr abs_eqn)) end;
+
+in
 
-val add_eqn = generic_add_eqn Strict;
-
-fun lift_attribute f = Thm.declaration_attribute
-  (fn thm => Context.mapping (f thm) I);
+fun generic_declare_eqns default strictness raw_eqns thy =
+  fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy;
 
-fun add_default_eqn_attribute kind =
-  lift_attribute (generic_add_eqn Silent (kind, true));
+fun generic_add_eqn strictness raw_eqn thy =
+  fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy;
 
-fun add_default_eqn_attrib kind =
-  Attrib.internal (K (add_default_eqn_attribute kind));
+fun generic_declare_abstract_eqn strictness raw_abs_eqn thy =
+  fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy;
 
 fun add_maybe_abs_eqn_liberal thm thy =
-  case mk_maybe_abs_eqn thy thm
-   of SOME (eqn, NONE) => gen_add_eqn false eqn thy
-    | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
+  case prep_maybe_abs_eqn thy thm
+   of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy
+    | SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy
     | NONE => thy;
 
-fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
- of SOME (thm, _) =>
+end;
+
+val declare_default_eqns_global = generic_declare_eqns true Silent;
+
+val declare_default_eqns =
+  silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true);
+
+val declare_eqns_global = generic_declare_eqns false Strict;
+
+val declare_eqns =
+  code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false);
+
+val add_eqn_global = generic_add_eqn Strict;
+
+fun del_eqn_global thm thy =
+  case prep_eqn Liberal thy (thm, false) of
+    SOME (c, (thm, _)) =>
       let
-        fun del_eqn' (Eqns_Default _) = default_fun_spec
-          | del_eqn' (Eqns eqns) =
+        fun del (Eqns_Default _) = Eqns []
+          | del (Eqns eqns) =
               Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
-          | del_eqn' spec = spec
-      in change_fun_spec (const_eqn thy thm) del_eqn' thy end
+          | del spec = spec
+      in change_fun_spec c del thy end
   | NONE => thy;
 
-val del_eqn_silent = generic_del_eqn Silent;
-val del_eqn = generic_del_eqn Liberal;
+val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
 
-fun del_eqns c = change_fun_spec c (K Unimplemented);
+val declare_abstract_eqn =
+  code_declaration Morphism.thm generic_declare_abstract_eqn;
 
-fun del_exception c = change_fun_spec c (K (Eqns []));
+fun declare_empty_global c = change_fun_spec c (K (Eqns []));
+
+fun declare_unimplemented_global c = change_fun_spec c (K Unimplemented);
 
 
 (* cases *)
@@ -1223,7 +1241,7 @@
         THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
   end;
 
-fun add_case thm thy =
+fun declare_case_global thm thy =
   let
     val (case_const, (k, cos)) = case_cert thm;
     val _ = case (filter_out (is_constr thy) o map_filter I) cos
@@ -1246,7 +1264,7 @@
     |-> (fn cong => map_spec_purge (register_case cong #> register_type))
   end;
 
-fun add_undefined c =
+fun declare_undefined_global c =
   (map_spec_purge o map_cases) (Symtab.update (c, Undefined));
 
 
@@ -1273,7 +1291,7 @@
           then insert (op =) c else I | _ => I) cases []) cases;
   in
     thy
-    |> fold del_eqns (outdated_funs1 @ outdated_funs2)
+    |> fold declare_unimplemented_global (outdated_funs1 @ outdated_funs2)
     |> map_spec_purge
         ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
         #> map_cases drop_outdated_cases)
@@ -1292,7 +1310,7 @@
       |> f (tyco, fst (get_type thy tyco))
       |> Sign.restore_naming thy));
 
-fun add_datatype proto_constrs thy =
+fun declare_datatype_global proto_constrs thy =
   let
     fun unoverload_const_typ (c, ty) =
       (Axclass.unoverload_const thy (c, ty), ty);
@@ -1304,8 +1322,8 @@
     |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
   end;
 
-fun add_datatype_cmd raw_constrs thy =
-  add_datatype (map (read_bare_const thy) raw_constrs) thy;
+fun declare_datatype_cmd raw_constrs thy =
+  declare_datatype_global (map (read_bare_const thy) raw_constrs) thy;
 
 structure Abstype_Plugin = Plugin(type T = string);
 
@@ -1316,35 +1334,48 @@
     (fn tyco =>
       Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
 
-fun generic_add_abstype strictness default proto_thm thy =
+fun generic_declare_abstype strictness proto_thm thy =
   case check_abstype_cert strictness thy proto_thm of
     SOME (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =>
       thy
       |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
       |> change_fun_spec rep
-        (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default)))
+        (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
       |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
   | NONE => thy;
 
-val add_abstype = generic_add_abstype Strict false;
-val add_abstype_default = generic_add_abstype Strict true;
+val declare_abstype_global = generic_declare_abstype Strict;
+
+val declare_abstype =
+  code_declaration Morphism.thm generic_declare_abstype;
 
 
 (* setup *)
 
+fun code_attribute f = Thm.declaration_attribute
+  (fn thm => Context.mapping (f thm) I);
+
+fun code_const_attribute f cs =
+  code_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
+
 val _ = Theory.setup
   (let
-    fun lift_const_attribute f cs =
-      lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
     val code_attribute_parser =
-      Args.$$$ "equation" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Equation, false)))
-      || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Nbe, false)))
-      || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Abstract, false)))
-      || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute (generic_add_abstype Liberal false))
-      || Args.del |-- Scan.succeed (lift_attribute del_eqn)
-      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns)
-      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception)
-      || Scan.succeed (lift_attribute add_maybe_abs_eqn_liberal);
+      Args.$$$ "equation" |-- Scan.succeed (code_attribute
+          (fn thm => generic_add_eqn Liberal (thm, true)))
+      || Args.$$$ "nbe" |-- Scan.succeed (code_attribute
+          (fn thm => generic_add_eqn Liberal (thm, false)))
+      || Args.$$$ "abstract" |-- Scan.succeed (code_attribute
+          (generic_declare_abstract_eqn Liberal))
+      || Args.$$$ "abstype" |-- Scan.succeed (code_attribute
+          (generic_declare_abstype Liberal))
+      || Args.del |-- Scan.succeed (code_attribute del_eqn_global)
+      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term
+          >> code_const_attribute declare_empty_global)
+      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term
+          >> code_const_attribute declare_unimplemented_global)
+      || Scan.succeed (code_attribute
+          add_maybe_abs_eqn_liberal);
   in
     Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
         "declare theorems for code generation"
diff -r 56a87a5093be -r cd935b7cb3fb src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -266,14 +266,17 @@
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])];
+      |> Local_Theory.notes [((name, atts), [([th], [])])];
 
-    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
+    val lthy5 = lthy4
+      |> Code.declare_default_eqns [(th', true)];
+
+    val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
 
     val _ =
-      Proof_Display.print_consts int (Position.thread_data ()) lthy4
+      Proof_Display.print_consts int (Position.thread_data ()) lthy5
         (member (op =) (Term.add_frees lhs' [])) [(x, T)];
-  in ((lhs, (def_name, th')), lthy4) end;
+  in ((lhs, (def_name, th')), lthy5) end;
 
 val definition' = gen_def check_spec_open (K I);
 fun definition xs ys As B = definition' xs ys As B false;
diff -r 56a87a5093be -r cd935b7cb3fb src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -802,7 +802,7 @@
              Logic.mk_equals (head, ft)), [])]
         |-> (fn [def_thm] =>
            Spec_Rules.add_global Spec_Rules.Equational ([head], [def_thm])
-           #> Code.add_eqn (Code.Equation, true) def_thm)
+           #> Code.declare_default_eqns_global [(def_thm, true)])
       end;
 
     fun add_corr (s, (vs, prf)) thy =
diff -r 56a87a5093be -r cd935b7cb3fb src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Pure/Pure.thy	Sun Jul 02 20:13:38 2017 +0200
@@ -1307,7 +1307,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword code_datatype}
     "define set of code datatype constructors"
-    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
+    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
 
 in end\<close>