diff -r 98e52f522357 -r f588e1169c8b src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -129,7 +129,7 @@
 
 fun preprocess thy =
   let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     preprocess_functrans thy
     #> (map o apfst) (rewrite_eqn pre)
@@ -137,7 +137,7 @@
 
 fun preprocess_conv thy ct =
   let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     ct
     |> Simplifier.rewrite pre
@@ -146,7 +146,7 @@
 
 fun postprocess_conv thy ct =
   let
-    val post = (Simplifier.theory_context thy o #post o the_thmproc) thy;
+    val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   in
     ct
     |> AxClass.overload_conv thy