diff -r c6d514717d7b -r ec5e62b868eb src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Jun 05 07:11:49 2012 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Jun 05 10:12:54 2012 +0200
@@ -14,7 +14,6 @@
   val del_functrans: string -> theory -> theory
   val simple_functrans: (theory -> thm list -> thm list option)
     -> theory -> (thm * bool) list -> (thm * bool) list option
-  val preprocess_functrans: theory -> (thm * bool) list -> (thm * bool) list
   val print_codeproc: theory -> unit
 
   type code_algebra
@@ -124,15 +123,6 @@
 
 fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
 
-fun eqn_conv conv ct =
-  let
-    fun lhs_conv ct = if can Thm.dest_comb ct
-      then Conv.combination_conv lhs_conv conv ct
-      else Conv.all_conv ct;
-  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
-
-val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
-
 fun term_of_conv thy conv =
   Thm.cterm_of thy
   #> conv
@@ -148,22 +138,6 @@
     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
-      o the_thmproc) thy;
-  in perhaps (perhaps_loop (perhaps_apply functrans)) end;
-
-fun preprocess thy =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
-  in
-    preprocess_functrans thy
-    #> (map o apfst) (singleton (Variable.trade (K (map (rewrite_eqn pre))) ctxt)) 
-  end;
-
 fun preprocess_conv thy =
   let
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
@@ -285,7 +259,10 @@
   case try (Graph.get_node eqngr) c
    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
-        val cert = Code.get_cert thy (preprocess thy) c;
+        val functrans = (map (fn (_, (_, f)) => f thy)
+          o #functrans o the_thmproc) thy;
+        val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
+        val cert = Code.get_cert thy { functrans = functrans, ss = pre } c;
         val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;