diff -r 842b5e7dcac8 -r 317663b422bb src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Jul 27 16:59:25 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sat Jul 27 18:02:41 2013 +0200
@@ -143,11 +143,13 @@
     val resubst = curry (Term.betapplys o swap) all_vars;
   in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
 
+fun lift_ss_conv f ss ct = f (Simplifier.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
+
 fun preprocess_conv thy =
   let
-    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
+    val pre = (#pre o the_thmproc) thy;
   in
-    Simplifier.rewrite pre
+    lift_ss_conv Simplifier.rewrite pre
     #> trans_conv_rule (Axclass.unoverload_conv thy)
   end;
 
@@ -155,10 +157,10 @@
 
 fun postprocess_conv thy =
   let
-    val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
+    val post = (#post o the_thmproc) thy;
   in
     Axclass.overload_conv thy
-    #> trans_conv_rule (Simplifier.rewrite post)
+    #> trans_conv_rule (lift_ss_conv Simplifier.rewrite post)
   end;
 
 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
@@ -484,11 +486,12 @@
   let
     val (algebra, eqngr) = obtain true thy consts [];
     val evaluator' = evaluator algebra eqngr;
+    val postproc' = postprocess_term thy;
   in 
     preprocess_term thy
     #-> (fn resubst => fn t => t
       |> evaluator' (Term.add_tfrees t [])
-      |> postproc (postprocess_term thy o resubst))
+      |> postproc (postproc' o resubst))
   end;