src/Tools/Code/code_preproc.ML
changeset 35232 f588e1169c8b
parent 34895 19fd499cddff
child 35235 7c7cfe69d7f6
--- 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