src/Tools/Code/code_preproc.ML
changeset 46026 83caa4f4bd56
parent 45230 1b08942bb86f
child 46497 89ccf66aa73d
     1.1 --- a/src/Tools/Code/code_preproc.ML	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -88,13 +88,13 @@
     1.4  val add_post = map_post o Simplifier.add_simp;
     1.5  val del_post = map_post o Simplifier.del_simp;
     1.6  
     1.7 -fun add_unfold_post raw_thm thy =
     1.8 +fun add_code_abbrev raw_thm thy =
     1.9    let
    1.10      val thm = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy) raw_thm;
    1.11      val thm_sym = Thm.symmetric thm;
    1.12    in
    1.13      thy |> map_pre_post (fn (pre, post) =>
    1.14 -      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
    1.15 +      (pre |> Simplifier.add_simp thm_sym, post |> Simplifier.add_simp thm))
    1.16    end;
    1.17  
    1.18  fun add_functrans (name, f) = (map_data o apsnd)
    1.19 @@ -520,8 +520,8 @@
    1.20          "preprocessing equations for code generator"
    1.21      #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
    1.22          "postprocessing equations for code generator"
    1.23 -    #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
    1.24 -        "pre- and postprocessing equations for code generator"
    1.25 +    #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
    1.26 +        "post- and preprocessing equations for code generator"
    1.27    end;
    1.28  
    1.29  val _ =