# HG changeset patch
# User haftmann
# Date 1282557442 -7200
# Node ID cd9b59cb1b755f5e85ed632ddc04f9d9bbd0cc47
# Parent  ae4c5d2512574d046ae2cfe04284ea96d173a6cb
dropped pre_post_conv

diff -r ae4c5d251257 -r cd9b59cb1b75 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:51:33 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:57:22 2010 +0200
@@ -30,7 +30,6 @@
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val static_eval_conv: theory -> string list
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
-  val pre_post_conv: theory -> conv -> conv
 
   val setup: theory -> theory
 end
@@ -457,15 +456,16 @@
 fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
   (K o postproc (postprocess_term thy)) (K oooo evaluator);
 
-fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
-
 fun static_eval_conv thy consts conv =
   let
     val (algebra, eqngr) = obtain thy consts [];
     fun conv' ct =
       let
         val (vs, t) = dest_cterm ct;
-      in Conv.tap_thy (fn thy => pre_post_conv thy (conv algebra eqngr vs t)) ct end;
+      in
+        Conv.tap_thy (fn thy => (preprocess_conv thy)
+          then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
+      end;
   in conv' end;