removing declaration of code_unfold to address the old code generator
authorbulwahn
Wed, 19 Oct 2011 09:11:19 +0200
changeset 45189 80cb73210612
parent 45188 35870ec62ec7
child 45190 58e33a125f32
removing declaration of code_unfold to address the old code generator
src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Oct 19 09:11:18 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Oct 19 09:11:19 2011 +0200
@@ -515,11 +515,9 @@
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     fun add_del_attribute_parser add del =
       Attrib.add_del (mk_attribute add) (mk_attribute del);
-    fun both f g thm = f thm #> g thm;
   in
-    Attrib.setup @{binding code_unfold} (add_del_attribute_parser 
-       (both Codegen.add_unfold add_unfold) (both Codegen.del_unfold del_unfold))
-        "preprocessing equations for code generators"
+    Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
+        "preprocessing equations for code generator"
     #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
         "preprocessing equations for code generator"
     #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)