explicit tagging of code equations de-baroquifies interface

--- a/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
@@ -242,7 +242,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML Code.read_const: "theory -> string -> string"} \\
-  @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
+  @{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"} \\
@@ -261,11 +261,11 @@
   \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 "thm"}~@{text "thy"} adds function
-     theorem @{text "thm"} to executable content.
+  \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 function
-     theorem @{text "thm"} from executable content, if present.
+  \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.

--- 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 .

--- a/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:46 2016 +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]
+        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
       else [];
     val ((simps' :: rules', [induct']), thy2) =
       Proof_Context.theory_of ctxt1

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1146,7 +1146,7 @@
             |> Proof_Context.export names_lthy lthy
           end;
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+        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)]
@@ -1577,7 +1577,7 @@
 
     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] else [];
+    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))
@@ -2234,7 +2234,7 @@
     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] else [];
+    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
 
     val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
     val ns = map length ctr_Tsss;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -2147,7 +2147,7 @@
           |> 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] else [];
+        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
 
         val anonymous_notes = [];
 (* TODO:

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1522,7 +1522,7 @@
         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] else [];
+        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)]

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -455,7 +455,7 @@
   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 :: @{attributes [nitpick_simp, simp]};
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]};
 
 fun datatype_compat fpT_names lthy =
   let

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -638,7 +638,7 @@
     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] else [];
+    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);
 

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -354,7 +354,7 @@
           end;
 
       (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
-      val code_attrs = Code.add_default_eqn_attrib;
+      val code_attrs = Code.add_default_eqn_attrib Code.Equation;
 
       val massage_multi_notes =
         maps (fn (thmN, thmss, attrs) =>

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1068,7 +1068,7 @@
         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] else [];
+        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]}

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -112,8 +112,8 @@
     #-> fold Code.del_eqn
     #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
     #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK
-      [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
-        ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+      [((qualify reflN, [Code.add_default_eqn_attribute Code.Nbe]), [([thm], [])]),
+        ((qualify simpsN, [Code.add_default_eqn_attribute Code.Equation]), [(rev thms, [])])])
     #> snd
   end;
 
@@ -127,7 +127,7 @@
     if can (Code.constrset_of_consts thy) unover_ctrs then
       thy
       |> Code.add_datatype ctrs
-      |> fold_rev Code.add_default_eqn case_thms
+      |> fold_rev (Code.add_eqn (Code.Equation, true)) case_thms
       |> Code.add_case (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

--- a/src/HOL/Tools/Function/function.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -45,7 +45,7 @@
 open Function_Common
 
 val simp_attribs =
-  @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)]
+  @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation]
 
 val psimp_attribs =
   @{attributes [nitpick_psimp]}

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -451,17 +451,17 @@
 
   in
     if is_valid_eq abs_eq_thm then
-      (ABS_EQ, Code.add_default_eqn abs_eq_thm thy)
+      (ABS_EQ, Code.add_eqn (Code.Equation, true) abs_eq_thm thy)
     else
       let
         val (rty_body, qty_body) = get_body_types (rty, qty)
       in
         if rty_body = qty_body then
-          (REP_EQ, Code.add_default_eqn (the opt_rep_eq_thm) thy)
+          (REP_EQ, Code.add_eqn (Code.Equation, true) (the opt_rep_eq_thm) thy)
         else
           if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
           then
-            (REP_EQ, Code.add_abs_default_eqn (the opt_rep_eq_thm) thy)
+            (REP_EQ, Code.add_eqn (Code.Abstract, true) (the opt_rep_eq_thm) thy)
           else
             (NONE_EQ, thy)
       end

--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -275,7 +275,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 :: attrs)) spec;
+      (Binding.qualify false prefix b, Code.add_default_eqn_attrib Code.Equation :: attrs)) spec;
     fun simp_attr_binding prefix =
       (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   in

--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -570,7 +570,7 @@
         ((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]), [(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), [])]),

--- a/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -196,8 +196,7 @@
           |> Global_Theory.note_thmss ""
             [((Binding.name "size",
                 [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
-                 Thm.declaration_attribute (fn thm =>
-                   Context.mapping (Code.add_default_eqn thm) I)]),
+                 Code.add_default_eqn_attribute Code.Equation]),
               [(size_eqns, [])])];
 
       in

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1421,7 +1421,9 @@
     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 thm) I)
+    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

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -111,7 +111,7 @@
   in
     thy
     |> Code.del_eqns const
-    |> fold Code.add_eqn eqs
+    |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*)
   end
 
 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -385,7 +385,7 @@
         fold (fn (name, eq) => Local_Theory.note
           ((Binding.qualify true prfx
               (Binding.qualify true name (Binding.name "simps")),
-             [Code.add_default_eqn_attrib]), [eq]) #> snd)
+             [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd)
           (names ~~ eqs) lthy
       end)
 

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -179,7 +179,7 @@
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> prove_simps
     |-> (fn simps => Local_Theory.note
-      ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
+      ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
     |> snd
   end
 

--- a/src/HOL/Tools/code_evaluation.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -93,7 +93,7 @@
  in
     thy
     |> Code.del_eqns const
-    |> fold Code.add_eqn eqs
+    |> fold (Code.add_eqn (Code.Equation, false)) eqs
   end;
 
 fun ensure_term_of_code (tyco, (vs, cs)) =
@@ -125,7 +125,7 @@
  in
     thy
     |> Code.del_eqns const
-    |> Code.add_eqn eq
+    |> Code.add_eqn (Code.Equation, false) eq
   end;
 
 fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =

--- a/src/HOL/Tools/record.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/record.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1778,7 +1778,7 @@
     in
       thy
       |> Code.add_datatype [ext]
-      |> fold Code.add_default_eqn simps
+      |> fold (Code.add_eqn (Code.Equation, true)) simps
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
@@ -1787,8 +1787,8 @@
       |-> (fn eq_def => fn thy =>
             thy
             |> Code.del_eqn eq_def
-            |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def))
-      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy)
+            |> 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)
       |> 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,7 +2045,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]
+                map (rpair [Code.add_default_eqn_attribute Code.Equation]
                 o apfst (Binding.concealed o Binding.name)))
             [make_spec, fields_spec, extend_spec, truncate_spec]);
     val defs_ctxt = Proof_Context.init_global defs_thy;

--- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -46,18 +46,13 @@
   val abstype_interpretation:
     (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
-  val add_eqn: thm -> theory -> theory
-  val add_nbe_eqn: thm -> theory -> theory
-  val add_abs_eqn: thm -> theory -> theory
-  val add_default_eqn: thm -> theory -> theory
-  val add_default_eqn_attribute: attribute
-  val add_default_eqn_attrib: Token.src
-  val add_nbe_default_eqn: thm -> theory -> theory
-  val add_nbe_default_eqn_attribute: attribute
-  val add_nbe_default_eqn_attrib: Token.src
-  val add_abs_default_eqn: thm -> theory -> theory
-  val add_abs_default_eqn_attribute: attribute
-  val add_abs_default_eqn_attrib: Token.src
+  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: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val del_exception: string -> theory -> theory
@@ -1073,6 +1068,14 @@
 
 (* code equations *)
 
+(*
+  external distinction:
+    kind * default
+  processual distinction:
+    thm * proper  for concrete equations
+    thm  for abstract equations
+*)
+
 fun gen_add_eqn default (raw_thm, proper) thy =
   let
     val thm = Thm.close_derivation raw_thm;
@@ -1112,34 +1115,25 @@
     val c = const_abs_eqn thy abs_thm;
   in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end;
 
-fun add_eqn thm thy =
-  gen_add_eqn false (mk_eqn thy (thm, true)) thy;
-
-fun add_nbe_eqn thm thy =
-  gen_add_eqn false (mk_eqn thy (thm, false)) thy;
-
-fun add_default_eqn thm thy =
-  case mk_eqn_liberal thy thm
-   of SOME eqn => gen_add_eqn true eqn thy
-    | NONE => thy;
+datatype kind = Equation | Nbe | Abstract;
 
-val add_default_eqn_attribute = Thm.declaration_attribute
-  (fn thm => Context.mapping (add_default_eqn thm) I);
-val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
-
-fun add_nbe_default_eqn thm thy =
-  gen_add_eqn true (mk_eqn thy (thm, false)) thy;
+fun add_eqn (kind, default) thm thy =
+  case (kind, default) of
+    (Equation, true) => (case mk_eqn_liberal thy thm of
+      SOME eqn => gen_add_eqn true eqn thy
+    | NONE => thy)
+  | (Equation, false) => gen_add_eqn false (mk_eqn thy (thm, true)) thy
+  | (Nbe, _) => gen_add_eqn default (mk_eqn thy (thm, false)) thy
+  | (Abstract, _) => gen_add_abs_eqn default (mk_abs_eqn thy thm) thy;
 
-val add_nbe_default_eqn_attribute = Thm.declaration_attribute
-  (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
-val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
+fun lift_attribute f = Thm.declaration_attribute
+  (fn thm => Context.mapping (f thm) I);
 
-fun add_abs_eqn raw_thm thy = gen_add_abs_eqn false (mk_abs_eqn thy raw_thm) thy;
-fun add_abs_default_eqn raw_thm thy = gen_add_abs_eqn true (mk_abs_eqn thy raw_thm) thy;
+fun add_default_eqn_attribute kind =
+  lift_attribute (add_eqn (kind, true));
 
-val add_abs_default_eqn_attribute = Thm.declaration_attribute
-  (fn thm => Context.mapping (add_abs_default_eqn thm) I);
-val add_abs_default_eqn_attrib = Attrib.internal (K add_abs_default_eqn_attribute);
+fun add_default_eqn_attrib kind =
+  Attrib.internal (K (add_default_eqn_attribute kind));
 
 fun add_eqn_maybe_abs thm thy =
   case mk_eqn_maybe_abs thy thm
@@ -1297,18 +1291,17 @@
 
 val _ = Theory.setup
   (let
-    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun mk_const_attribute f cs =
-      mk_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
+    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 (mk_attribute add_eqn)
-      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
-      || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
-      || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
-      || Args.del |-- Scan.succeed (mk_attribute del_eqn)
-      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_eqns)
-      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception)
-      || Scan.succeed (mk_attribute add_eqn_maybe_abs);
+      Args.$$$ "equation" |-- Scan.succeed (lift_attribute (add_eqn (Equation, false)))
+      || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (add_eqn (Nbe, false)))
+      || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (add_eqn (Abstract, false)))
+      || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute add_abstype)
+      || 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_eqn_maybe_abs);
   in
     Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
         "declare theorems for code generation"

--- a/src/Pure/Isar/specification.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -260,7 +260,7 @@
     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 :: atts), [([th], [])])];
+      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
 

--- a/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -810,7 +810,7 @@
                       (Proof_Checker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
-             |> fold Code.add_default_eqn def_thms
+             |> fold (Code.add_eqn (Code.Equation, true)) def_thms
            end
        | SOME _ => thy);