Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/Code/code_preproc.ML
changeset 35235 7c7cfe69d7f6
parent 35224 1c9866c5f6fb
parent 35232 f588e1169c8b
child 35624 c4e29a0bb8c1 
--- a/src/Tools/Code/code_preproc.ML	Fri Feb 19 16:42:37 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Feb 19 17:03:53 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
isabelle