explicit tagging of code equations de-baroquifies interface
authorhaftmann
Mon Jun 06 21:28:46 2016 +0200 (2016-06-06)
changeset 63239d562c9948dee
parent 63238 7c593d4f1f89
child 63240 f82c0b803bda
explicit tagging of code equations de-baroquifies interface
src/Doc/Codegen/Further.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/old_recdef.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Old_Datatype/old_primrec.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Old_Datatype/old_size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/record.ML
src/Pure/Isar/code.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:45 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
     1.3 @@ -242,7 +242,7 @@
     1.4  text %mlref \<open>
     1.5    \begin{mldecls}
     1.6    @{index_ML Code.read_const: "theory -> string -> string"} \\
     1.7 -  @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
     1.8 +  @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\
     1.9    @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
    1.10    @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.11    @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.12 @@ -261,11 +261,11 @@
    1.13    \item @{ML Code.read_const}~@{text thy}~@{text s}
    1.14       reads a constant as a concrete term expression @{text s}.
    1.15  
    1.16 -  \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
    1.17 -     theorem @{text "thm"} to executable content.
    1.18 +  \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation
    1.19 +     @{text "thm"} to executable content.
    1.20  
    1.21 -  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
    1.22 -     theorem @{text "thm"} from executable content, if present.
    1.23 +  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation
    1.24 +     @{text "thm"} from executable content, if present.
    1.25  
    1.26    \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
    1.27       the preprocessor simpset.
     2.1 --- a/src/HOL/Library/Mapping.thy	Mon Jun 06 21:28:45 2016 +0200
     2.2 +++ b/src/HOL/Library/Mapping.thy	Mon Jun 06 21:28:46 2016 +0200
     2.3 @@ -121,7 +121,7 @@
     2.4  definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
     2.5  
     2.6  declare [[code drop: Mapping.lookup]]
     2.7 -setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
     2.8 +setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
     2.9  
    2.10  lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
    2.11    is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
     3.1 --- a/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:45 2016 +0200
     3.2 +++ b/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:46 2016 +0200
     3.3 @@ -2834,7 +2834,7 @@
     3.4      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     3.5      val simp_att =
     3.6        if null tcs then [Simplifier.simp_add,
     3.7 -        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
     3.8 +        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
     3.9        else [];
    3.10      val ((simps' :: rules', [induct']), thy2) =
    3.11        Proof_Context.theory_of ctxt1
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
     4.3 @@ -1146,7 +1146,7 @@
     4.4              |> Proof_Context.export names_lthy lthy
     4.5            end;
     4.6  
     4.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
     4.8 +        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
     4.9  
    4.10          val anonymous_notes =
    4.11            [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
    4.12 @@ -1577,7 +1577,7 @@
    4.13  
    4.14      val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
    4.15  
    4.16 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    4.17 +    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    4.18    in
    4.19      ((induct_thms, induct_thm, mk_induct_attrs ctrss),
    4.20       (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
    4.21 @@ -2234,7 +2234,7 @@
    4.22      val fpTs = map (domain_type o fastype_of) dtors;
    4.23      val fpBTs = map B_ify_T fpTs;
    4.24  
    4.25 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    4.26 +    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    4.27  
    4.28      val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
    4.29      val ns = map length ctr_Tsss;
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
     5.3 @@ -2147,7 +2147,7 @@
     5.4            |> derive_and_update_coinduct_cong_intross [corec_info];
     5.5          val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
     5.6  
     5.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
     5.8 +        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
     5.9  
    5.10          val anonymous_notes = [];
    5.11  (* TODO:
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
     6.3 @@ -1522,7 +1522,7 @@
     6.4          val common_name = mk_common_name fun_names;
     6.5          val common_qualify = fold_rev I qualifys;
     6.6  
     6.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
     6.8 +        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
     6.9  
    6.10          val anonymous_notes =
    6.11            [(flat disc_iff_or_disc_thmss, simp_attrs)]
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:45 2016 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:46 2016 +0200
     7.3 @@ -455,7 +455,7 @@
     7.4    Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
     7.5    #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
     7.6  
     7.7 -val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
     7.8 +val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]};
     7.9  
    7.10  fun datatype_compat fpT_names lthy =
    7.11    let
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
     8.3 @@ -638,7 +638,7 @@
     8.4      val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
     8.5      val transfer = exists (can (fn Transfer_Option => ())) opts;
     8.6  
     8.7 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
     8.8 +    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
     8.9  
    8.10      val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
    8.11  
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 06 21:28:45 2016 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 06 21:28:46 2016 +0200
     9.3 @@ -354,7 +354,7 @@
     9.4            end;
     9.5  
     9.6        (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
     9.7 -      val code_attrs = Code.add_default_eqn_attrib;
     9.8 +      val code_attrs = Code.add_default_eqn_attrib Code.Equation;
     9.9  
    9.10        val massage_multi_notes =
    9.11          maps (fn (thmN, thmss, attrs) =>
    10.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
    10.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
    10.3 @@ -1068,7 +1068,7 @@
    10.4          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    10.5          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
    10.6  
    10.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    10.8 +        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    10.9  
   10.10          val nontriv_disc_eq_thmss =
   10.11            map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    11.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jun 06 21:28:45 2016 +0200
    11.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jun 06 21:28:46 2016 +0200
    11.3 @@ -112,8 +112,8 @@
    11.4      #-> fold Code.del_eqn
    11.5      #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
    11.6      #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK
    11.7 -      [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
    11.8 -        ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
    11.9 +      [((qualify reflN, [Code.add_default_eqn_attribute Code.Nbe]), [([thm], [])]),
   11.10 +        ((qualify simpsN, [Code.add_default_eqn_attribute Code.Equation]), [(rev thms, [])])])
   11.11      #> snd
   11.12    end;
   11.13  
   11.14 @@ -127,7 +127,7 @@
   11.15      if can (Code.constrset_of_consts thy) unover_ctrs then
   11.16        thy
   11.17        |> Code.add_datatype ctrs
   11.18 -      |> fold_rev Code.add_default_eqn case_thms
   11.19 +      |> fold_rev (Code.add_eqn (Code.Equation, true)) case_thms
   11.20        |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms)
   11.21        |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
   11.22          ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
    12.1 --- a/src/HOL/Tools/Function/function.ML	Mon Jun 06 21:28:45 2016 +0200
    12.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Jun 06 21:28:46 2016 +0200
    12.3 @@ -45,7 +45,7 @@
    12.4  open Function_Common
    12.5  
    12.6  val simp_attribs =
    12.7 -  @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)]
    12.8 +  @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation]
    12.9  
   12.10  val psimp_attribs =
   12.11    @{attributes [nitpick_psimp]}
    13.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jun 06 21:28:45 2016 +0200
    13.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jun 06 21:28:46 2016 +0200
    13.3 @@ -451,17 +451,17 @@
    13.4  
    13.5    in
    13.6      if is_valid_eq abs_eq_thm then
    13.7 -      (ABS_EQ, Code.add_default_eqn abs_eq_thm thy)
    13.8 +      (ABS_EQ, Code.add_eqn (Code.Equation, true) abs_eq_thm thy)
    13.9      else
   13.10        let
   13.11          val (rty_body, qty_body) = get_body_types (rty, qty)
   13.12        in
   13.13          if rty_body = qty_body then
   13.14 -          (REP_EQ, Code.add_default_eqn (the opt_rep_eq_thm) thy)
   13.15 +          (REP_EQ, Code.add_eqn (Code.Equation, true) (the opt_rep_eq_thm) thy)
   13.16          else
   13.17            if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
   13.18            then
   13.19 -            (REP_EQ, Code.add_abs_default_eqn (the opt_rep_eq_thm) thy)
   13.20 +            (REP_EQ, Code.add_eqn (Code.Abstract, true) (the opt_rep_eq_thm) thy)
   13.21            else
   13.22              (NONE_EQ, thy)
   13.23        end
    14.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jun 06 21:28:45 2016 +0200
    14.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jun 06 21:28:46 2016 +0200
    14.3 @@ -275,7 +275,7 @@
    14.4    let
    14.5      val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
    14.6      fun attr_bindings prefix = map (fn ((b, attrs), _) =>
    14.7 -      (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
    14.8 +      (Binding.qualify false prefix b, Code.add_default_eqn_attrib Code.Equation :: attrs)) spec;
    14.9      fun simp_attr_binding prefix =
   14.10        (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   14.11    in
    15.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jun 06 21:28:45 2016 +0200
    15.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jun 06 21:28:46 2016 +0200
    15.3 @@ -570,7 +570,7 @@
    15.4          ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
    15.5          ((Binding.empty, [Simplifier.simp_add]),
    15.6            [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
    15.7 -        ((Binding.empty, [Code.add_default_eqn_attribute]), [(rec_rewrites, [])]),
    15.8 +        ((Binding.empty, [Code.add_default_eqn_attribute Code.Equation]), [(rec_rewrites, [])]),
    15.9          ((Binding.empty, [iff_add]), [(flat inject, [])]),
   15.10          ((Binding.empty, [Classical.safe_elim NONE]),
   15.11            [(map (fn th => th RS notE) (flat distinct), [])]),
    16.1 --- a/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:45 2016 +0200
    16.2 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:46 2016 +0200
    16.3 @@ -196,8 +196,7 @@
    16.4            |> Global_Theory.note_thmss ""
    16.5              [((Binding.name "size",
    16.6                  [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
    16.7 -                 Thm.declaration_attribute (fn thm =>
    16.8 -                   Context.mapping (Code.add_default_eqn thm) I)]),
    16.9 +                 Code.add_default_eqn_attribute Code.Equation]),
   16.10                [(size_eqns, [])])];
   16.11  
   16.12        in
    17.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 06 21:28:45 2016 +0200
    17.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 06 21:28:46 2016 +0200
    17.3 @@ -1421,7 +1421,9 @@
    17.4      val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
    17.5        (maps_modes result_thms)
    17.6      val qname = #qname (dest_steps steps)
    17.7 -    val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)
    17.8 +    val attrib = Thm.declaration_attribute (fn thm => Context.mapping
    17.9 +      (Code.add_eqn (Code.Equation, false) thm) I)
   17.10 +      (*FIXME default code equation!?*)
   17.11      val thy''' =
   17.12        cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
   17.13        fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
    18.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 21:28:45 2016 +0200
    18.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 21:28:46 2016 +0200
    18.3 @@ -111,7 +111,7 @@
    18.4    in
    18.5      thy
    18.6      |> Code.del_eqns const
    18.7 -    |> fold Code.add_eqn eqs
    18.8 +    |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*)
    18.9    end
   18.10  
   18.11  fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
    19.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jun 06 21:28:45 2016 +0200
    19.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jun 06 21:28:46 2016 +0200
    19.3 @@ -385,7 +385,7 @@
    19.4          fold (fn (name, eq) => Local_Theory.note
    19.5            ((Binding.qualify true prfx
    19.6                (Binding.qualify true name (Binding.name "simps")),
    19.7 -             [Code.add_default_eqn_attrib]), [eq]) #> snd)
    19.8 +             [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd)
    19.9            (names ~~ eqs) lthy
   19.10        end)
   19.11  
    20.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:45 2016 +0200
    20.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:46 2016 +0200
    20.3 @@ -179,7 +179,7 @@
    20.4      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
    20.5      |-> prove_simps
    20.6      |-> (fn simps => Local_Theory.note
    20.7 -      ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
    20.8 +      ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
    20.9      |> snd
   20.10    end
   20.11  
    21.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Jun 06 21:28:45 2016 +0200
    21.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Jun 06 21:28:46 2016 +0200
    21.3 @@ -93,7 +93,7 @@
    21.4   in
    21.5      thy
    21.6      |> Code.del_eqns const
    21.7 -    |> fold Code.add_eqn eqs
    21.8 +    |> fold (Code.add_eqn (Code.Equation, false)) eqs
    21.9    end;
   21.10  
   21.11  fun ensure_term_of_code (tyco, (vs, cs)) =
   21.12 @@ -125,7 +125,7 @@
   21.13   in
   21.14      thy
   21.15      |> Code.del_eqns const
   21.16 -    |> Code.add_eqn eq
   21.17 +    |> Code.add_eqn (Code.Equation, false) eq
   21.18    end;
   21.19  
   21.20  fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =
    22.1 --- a/src/HOL/Tools/record.ML	Mon Jun 06 21:28:45 2016 +0200
    22.2 +++ b/src/HOL/Tools/record.ML	Mon Jun 06 21:28:46 2016 +0200
    22.3 @@ -1778,7 +1778,7 @@
    22.4      in
    22.5        thy
    22.6        |> Code.add_datatype [ext]
    22.7 -      |> fold Code.add_default_eqn simps
    22.8 +      |> fold (Code.add_eqn (Code.Equation, true)) simps
    22.9        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   22.10        |> `(fn lthy => Syntax.check_term lthy eq)
   22.11        |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
   22.12 @@ -1787,8 +1787,8 @@
   22.13        |-> (fn eq_def => fn thy =>
   22.14              thy
   22.15              |> Code.del_eqn eq_def
   22.16 -            |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def))
   22.17 -      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy)
   22.18 +            |> Code.add_eqn (Code.Equation, true) (mk_eq (Proof_Context.init_global thy) eq_def))
   22.19 +      |> (fn thy => Code.add_eqn (Code.Nbe, true) (mk_eq_refl (Proof_Context.init_global thy)) thy)
   22.20        |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
   22.21        |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
   22.22      end
   22.23 @@ -2045,7 +2045,7 @@
   22.24            ||>> (Global_Theory.add_defs false o
   22.25                  map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
   22.26            ||>> (Global_Theory.add_defs false o
   22.27 -                map (rpair [Code.add_default_eqn_attribute]
   22.28 +                map (rpair [Code.add_default_eqn_attribute Code.Equation]
   22.29                  o apfst (Binding.concealed o Binding.name)))
   22.30              [make_spec, fields_spec, extend_spec, truncate_spec]);
   22.31      val defs_ctxt = Proof_Context.init_global defs_thy;
    23.1 --- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:45 2016 +0200
    23.2 +++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
    23.3 @@ -46,18 +46,13 @@
    23.4    val abstype_interpretation:
    23.5      (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
    23.6        -> theory -> theory) -> theory -> theory
    23.7 -  val add_eqn: thm -> theory -> theory
    23.8 -  val add_nbe_eqn: thm -> theory -> theory
    23.9 -  val add_abs_eqn: thm -> theory -> theory
   23.10 -  val add_default_eqn: thm -> theory -> theory
   23.11 -  val add_default_eqn_attribute: attribute
   23.12 -  val add_default_eqn_attrib: Token.src
   23.13 -  val add_nbe_default_eqn: thm -> theory -> theory
   23.14 -  val add_nbe_default_eqn_attribute: attribute
   23.15 -  val add_nbe_default_eqn_attrib: Token.src
   23.16 -  val add_abs_default_eqn: thm -> theory -> theory
   23.17 -  val add_abs_default_eqn_attribute: attribute
   23.18 -  val add_abs_default_eqn_attrib: Token.src
   23.19 +  type kind
   23.20 +  val Equation: kind
   23.21 +  val Nbe: kind
   23.22 +  val Abstract: kind
   23.23 +  val add_eqn: kind * bool -> thm -> theory -> theory
   23.24 +  val add_default_eqn_attribute: kind -> attribute
   23.25 +  val add_default_eqn_attrib: kind -> Token.src
   23.26    val del_eqn: thm -> theory -> theory
   23.27    val del_eqns: string -> theory -> theory
   23.28    val del_exception: string -> theory -> theory
   23.29 @@ -1073,6 +1068,14 @@
   23.30  
   23.31  (* code equations *)
   23.32  
   23.33 +(*
   23.34 +  external distinction:
   23.35 +    kind * default
   23.36 +  processual distinction:
   23.37 +    thm * proper  for concrete equations
   23.38 +    thm  for abstract equations
   23.39 +*)
   23.40 +
   23.41  fun gen_add_eqn default (raw_thm, proper) thy =
   23.42    let
   23.43      val thm = Thm.close_derivation raw_thm;
   23.44 @@ -1112,34 +1115,25 @@
   23.45      val c = const_abs_eqn thy abs_thm;
   23.46    in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end;
   23.47  
   23.48 -fun add_eqn thm thy =
   23.49 -  gen_add_eqn false (mk_eqn thy (thm, true)) thy;
   23.50 -
   23.51 -fun add_nbe_eqn thm thy =
   23.52 -  gen_add_eqn false (mk_eqn thy (thm, false)) thy;
   23.53 -
   23.54 -fun add_default_eqn thm thy =
   23.55 -  case mk_eqn_liberal thy thm
   23.56 -   of SOME eqn => gen_add_eqn true eqn thy
   23.57 -    | NONE => thy;
   23.58 +datatype kind = Equation | Nbe | Abstract;
   23.59  
   23.60 -val add_default_eqn_attribute = Thm.declaration_attribute
   23.61 -  (fn thm => Context.mapping (add_default_eqn thm) I);
   23.62 -val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
   23.63 -
   23.64 -fun add_nbe_default_eqn thm thy =
   23.65 -  gen_add_eqn true (mk_eqn thy (thm, false)) thy;
   23.66 +fun add_eqn (kind, default) thm thy =
   23.67 +  case (kind, default) of
   23.68 +    (Equation, true) => (case mk_eqn_liberal thy thm of
   23.69 +      SOME eqn => gen_add_eqn true eqn thy
   23.70 +    | NONE => thy)
   23.71 +  | (Equation, false) => gen_add_eqn false (mk_eqn thy (thm, true)) thy
   23.72 +  | (Nbe, _) => gen_add_eqn default (mk_eqn thy (thm, false)) thy
   23.73 +  | (Abstract, _) => gen_add_abs_eqn default (mk_abs_eqn thy thm) thy;
   23.74  
   23.75 -val add_nbe_default_eqn_attribute = Thm.declaration_attribute
   23.76 -  (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
   23.77 -val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
   23.78 +fun lift_attribute f = Thm.declaration_attribute
   23.79 +  (fn thm => Context.mapping (f thm) I);
   23.80  
   23.81 -fun add_abs_eqn raw_thm thy = gen_add_abs_eqn false (mk_abs_eqn thy raw_thm) thy;
   23.82 -fun add_abs_default_eqn raw_thm thy = gen_add_abs_eqn true (mk_abs_eqn thy raw_thm) thy;
   23.83 +fun add_default_eqn_attribute kind =
   23.84 +  lift_attribute (add_eqn (kind, true));
   23.85  
   23.86 -val add_abs_default_eqn_attribute = Thm.declaration_attribute
   23.87 -  (fn thm => Context.mapping (add_abs_default_eqn thm) I);
   23.88 -val add_abs_default_eqn_attrib = Attrib.internal (K add_abs_default_eqn_attribute);
   23.89 +fun add_default_eqn_attrib kind =
   23.90 +  Attrib.internal (K (add_default_eqn_attribute kind));
   23.91  
   23.92  fun add_eqn_maybe_abs thm thy =
   23.93    case mk_eqn_maybe_abs thy thm
   23.94 @@ -1297,18 +1291,17 @@
   23.95  
   23.96  val _ = Theory.setup
   23.97    (let
   23.98 -    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   23.99 -    fun mk_const_attribute f cs =
  23.100 -      mk_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
  23.101 +    fun lift_const_attribute f cs =
  23.102 +      lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
  23.103      val code_attribute_parser =
  23.104 -      Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_eqn)
  23.105 -      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
  23.106 -      || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
  23.107 -      || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
  23.108 -      || Args.del |-- Scan.succeed (mk_attribute del_eqn)
  23.109 -      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_eqns)
  23.110 -      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception)
  23.111 -      || Scan.succeed (mk_attribute add_eqn_maybe_abs);
  23.112 +      Args.$$$ "equation" |-- Scan.succeed (lift_attribute (add_eqn (Equation, false)))
  23.113 +      || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (add_eqn (Nbe, false)))
  23.114 +      || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (add_eqn (Abstract, false)))
  23.115 +      || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute add_abstype)
  23.116 +      || Args.del |-- Scan.succeed (lift_attribute del_eqn)
  23.117 +      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns)
  23.118 +      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception)
  23.119 +      || Scan.succeed (lift_attribute add_eqn_maybe_abs);
  23.120    in
  23.121      Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
  23.122          "declare theorems for code generation"
    24.1 --- a/src/Pure/Isar/specification.ML	Mon Jun 06 21:28:45 2016 +0200
    24.2 +++ b/src/Pure/Isar/specification.ML	Mon Jun 06 21:28:46 2016 +0200
    24.3 @@ -260,7 +260,7 @@
    24.4      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
    24.5  
    24.6      val ([(def_name, [th'])], lthy4) = lthy3
    24.7 -      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
    24.8 +      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])];
    24.9  
   24.10      val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
   24.11  
    25.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:45 2016 +0200
    25.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:46 2016 +0200
    25.3 @@ -810,7 +810,7 @@
    25.4                        (Proof_Checker.thm_of_proof thy'
    25.5                         (fst (Proofterm.freeze_thaw_prf prf))))))
    25.6               |> snd
    25.7 -             |> fold Code.add_default_eqn def_thms
    25.8 +             |> fold (Code.add_eqn (Code.Equation, true)) def_thms
    25.9             end
   25.10         | SOME _ => thy);
   25.11