code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
1.1 --- a/src/Tools/Code/code_preproc.ML Wed Jun 01 00:23:16 2011 +0200
1.2 +++ b/src/Tools/Code/code_preproc.ML Wed Jun 01 08:07:27 2011 +0200
1.3 @@ -157,15 +157,15 @@
1.4
1.5 fun preprocess thy =
1.6 let
1.7 + val ctxt = Proof_Context.init_global thy;
1.8 val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
1.9 in
1.10 preprocess_functrans thy
1.11 - #> (map o apfst) (rewrite_eqn pre)
1.12 + #> (map o apfst) (singleton (Variable.trade (K (map (rewrite_eqn pre))) ctxt))
1.13 end;
1.14
1.15 fun preprocess_conv thy =
1.16 let
1.17 - val ctxt = Proof_Context.init_global thy;
1.18 val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
1.19 in
1.20 Simplifier.rewrite pre