--- 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