code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps

--- a/src/Tools/Code/code_preproc.ML	Wed Jun 01 00:23:16 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Jun 01 08:07:27 2011 +0200
@@ -157,15 +157,15 @@
 
 fun preprocess thy =
   let
+    val ctxt = Proof_Context.init_global thy;
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     preprocess_functrans thy
-    #> (map o apfst) (rewrite_eqn pre)
+    #> (map o apfst) (singleton (Variable.trade (K (map (rewrite_eqn pre))) ctxt)) 
   end;
 
 fun preprocess_conv thy =
   let
-    val ctxt = Proof_Context.init_global thy;
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     Simplifier.rewrite pre