1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri May 09 08:13:37 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri May 09 08:13:37 2014 +0200
     1.3 @@ -2606,7 +2606,8 @@
     1.4    "del"}'' removes) theorems which are applied as rewrite rules to any
     1.5    result of an evaluation.
     1.6  
     1.7 -  \item @{attribute (HOL) code_abbrev} declares equations which are
     1.8 +  \item @{attribute (HOL) code_abbrev} declares (or with option ``@{text
     1.9 +  "del"}'' removes) equations which are
    1.10    applied as rewrite rules to any result of an evaluation and
    1.11    symmetrically during preprocessing to any code equation or evaluation
    1.12    input.

     2.1 --- a/src/Tools/Code/code_preproc.ML	Fri May 09 08:13:37 2014 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Fri May 09 08:13:37 2014 +0200
     2.3 @@ -9,7 +9,6 @@
     2.4  sig
     2.5    val map_pre: (Proof.context -> Proof.context) -> theory -> theory
     2.6    val map_post: (Proof.context -> Proof.context) -> theory -> theory
     2.7 -  val add_unfold: thm -> theory -> theory
     2.8    val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
     2.9    val del_functrans: string -> theory -> theory
    2.10    val simple_functrans: (Proof.context -> thm list -> thm list option)
    2.11 @@ -87,20 +86,18 @@
    2.12  val map_pre = map_simpset apfst;
    2.13  val map_post = map_simpset apsnd;
    2.14  
    2.15 -val add_unfold = map_pre o Simplifier.add_simp;
    2.16 -val del_unfold = map_pre o Simplifier.del_simp;
    2.17 -val add_post = map_post o Simplifier.add_simp;
    2.18 -val del_post = map_post o Simplifier.del_simp;
    2.19 +fun process_unfold add_del = map_pre o add_del;
    2.20 +fun process_post add_del = map_post o add_del;
    2.21  
    2.22 -fun add_code_abbrev raw_thm thy =
    2.23 +fun process_abbrev add_del raw_thm thy =
    2.24    let
    2.25      val ctxt = Proof_Context.init_global thy;
    2.26      val thm = Local_Defs.meta_rewrite_rule ctxt raw_thm;
    2.27      val thm_sym = Thm.symmetric thm;
    2.28    in
    2.29      thy |> map_pre_post (fn (pre, post) =>
    2.30 -      (pre |> simpset_map ctxt (Simplifier.add_simp thm_sym),
    2.31 -       post |> simpset_map ctxt (Simplifier.add_simp thm)))
    2.32 +      (pre |> simpset_map ctxt (add_del thm_sym),
    2.33 +       post |> simpset_map ctxt (add_del thm)))
    2.34    end;
    2.35  
    2.36  fun add_functrans (name, f) = (map_data o apsnd)
    2.37 @@ -520,14 +517,15 @@
    2.38  val setup = 
    2.39    let
    2.40      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    2.41 -    fun add_del_attribute_parser add del =
    2.42 -      Attrib.add_del (mk_attribute add) (mk_attribute del);
    2.43 +    fun add_del_attribute_parser process =
    2.44 +      Attrib.add_del (mk_attribute (process Simplifier.add_simp))
    2.45 +        (mk_attribute (process Simplifier.del_simp));
    2.46    in
    2.47 -    Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
    2.48 +    Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
    2.49          "preprocessing equations for code generator"
    2.50 -    #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
    2.51 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
    2.52          "postprocessing equations for code generator"
    2.53 -    #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
    2.54 +    #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
    2.55          "post- and preprocessing equations for code generator"
    2.56    end;
    2.57