src/Tools/Code/code_preproc.ML

   val add_unfold: thm -> theory -> theory
   val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
   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
   type code_graph
   val cert: code_graph -> string -> Code.cert

   #> f
   #> Thm.prop_of
   #> Logic.dest_equals
   #> snd;
 
-fun preprocess thy eqns =
-  let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+fun preprocess_functrans thy = 
+  let
     val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
       o the_thmproc) thy;
-  in
-    eqns
-    |> perhaps (perhaps_loop (perhaps_apply functrans))
-    |> (map o apfst) (rewrite_eqn pre)
+  in perhaps (perhaps_loop (perhaps_apply functrans)) end;
+
+fun preprocess thy =
+  let
+    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+  in
+    preprocess_functrans thy
+    #> (map o apfst) (rewrite_eqn pre)
   end;
 
 fun preprocess_conv thy ct =
   let
     val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;