diff -r 7cded8957e72 -r ba1eac745c5a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Dec 16 09:28:19 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Thu Dec 16 09:40:15 2010 +0100
@@ -133,13 +133,22 @@
 
 val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
 
-fun term_of_conv thy f =
+fun term_of_conv thy conv =
   Thm.cterm_of thy
-  #> f
+  #> conv
   #> Thm.prop_of
   #> Logic.dest_equals
   #> snd;
 
+fun term_of_conv_resubst thy conv t =
+  let
+    val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
+      | t as Var _ => insert (op aconv) t
+      | _ => I) t [];
+    val resubst = curry (Term.betapplys o swap) all_vars;
+  in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
+
+
 fun preprocess_functrans thy = 
   let
     val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
@@ -154,31 +163,23 @@
     #> (map o apfst) (rewrite_eqn pre)
   end;
 
-fun preprocess_conv thy ct =
+fun preprocess_conv thy =
   let
     val ctxt = ProofContext.init_global thy;
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
-    ct
-    |> Simplifier.rewrite pre
-    |> trans_conv_rule (AxClass.unoverload_conv thy)
+    Simplifier.rewrite pre
+    #> trans_conv_rule (AxClass.unoverload_conv thy)
   end;
 
-fun preprocess_term thy t =
-  let
-    val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
-      | t as Var _ => insert (op aconv) t
-      | _ => I) t [];
-    val resubst = curry (Term.betapplys o swap) all_vars;
-  in (resubst, term_of_conv thy (preprocess_conv thy) (fold_rev lambda all_vars t)) end;
+fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
 
-fun postprocess_conv thy ct =
+fun postprocess_conv thy =
   let
     val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   in
-    ct
-    |> AxClass.overload_conv thy
-    |> trans_conv_rule (Simplifier.rewrite post)
+    AxClass.overload_conv thy
+    #> trans_conv_rule (Simplifier.rewrite post)
   end;
 
 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
@@ -489,23 +490,22 @@
 fun static_conv thy consts conv =
   let
     val (algebra, eqngr) = obtain true thy consts [];
-    val conv' = conv algebra eqngr;
+    val conv' = conv algebra eqngr thy;
   in
-    no_variables_conv (Conv.tap_thy (fn thy => (preprocess_conv thy)
-      then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
-      then_conv (postprocess_conv thy)))
+    no_variables_conv ((preprocess_conv thy)
+      then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
+      then_conv (postprocess_conv thy))
   end;
 
 fun static_value thy postproc consts evaluator =
   let
     val (algebra, eqngr) = obtain true thy consts [];
     val evaluator' = evaluator algebra eqngr;
-  in fn t =>
-    t
-    |> preprocess_term thy
-    |-> (fn resubst => fn t => t
-    |> evaluator' thy (Term.add_tfrees t [])
-    |> postproc (postprocess_term thy o resubst))
+  in 
+    preprocess_term thy
+    #-> (fn resubst => fn t => t
+      |> evaluator' thy (Term.add_tfrees t [])
+      |> postproc (postprocess_term thy o resubst))
   end;