# HG changeset patch
# User bulwahn
# Date 1319008279 -7200
# Node ID 80cb732106121d3db9861d181ad469fa23196fab
# Parent  35870ec62ec769f59b9b2890b1a99dace92ec364
removing declaration of code_unfold to address the old code generator

diff -r 35870ec62ec7 -r 80cb73210612 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)