# HG changeset patch
# User haftmann
# Date 1263374325 -3600
# Node ID ecdc526af73aeaf8b47ad0ee8aa162c451af31d2
# Parent  6144d233b99afe745adca8833f6030233ad52f7b
function transformer preprocessor applies to both code generators

diff -r 6144d233b99a -r ecdc526af73a src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 09:13:30 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 10:18:45 2010 +0100
@@ -161,7 +161,7 @@
       end
   in get_first mk_thms eqs end;
 
-fun eqn_suc_preproc thy thms =
+fun eqn_suc_base_preproc thy thms =
   let
     val dest = fst o Logic.dest_equals o prop_of;
     val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
@@ -171,10 +171,7 @@
        else NONE
   end;
 
-val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc;
-
-fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms
-  |> the_default thms;
+val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
 
 fun remove_suc_clause thy thms =
   let
@@ -217,9 +214,8 @@
   end;
 in
 
-  Codegen.add_preprocessor eqn_suc_preproc2
+  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
   #> Codegen.add_preprocessor clause_suc_preproc
-  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1)
 
 end;
 *}
diff -r 6144d233b99a -r ecdc526af73a src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 09:13:30 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 10:18:45 2010 +0100
@@ -43,7 +43,7 @@
 fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
   let
     val c = AxClass.unoverload_const thy (raw_c, T);
-    val raw_thms = Code.get_cert thy I c
+    val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
       |> Code.eqns_of_cert thy
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> map (AxClass.overload thy)
diff -r 6144d233b99a -r ecdc526af73a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Jan 13 09:13:30 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Wed Jan 13 10:18:45 2010 +0100
@@ -14,6 +14,7 @@
   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
@@ -120,15 +121,18 @@
   #> Logic.dest_equals
   #> snd;
 
-fun preprocess thy eqns =
+fun preprocess_functrans thy = 
   let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
     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 pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
   in
-    eqns
-    |> perhaps (perhaps_loop (perhaps_apply functrans))
-    |> (map o apfst) (rewrite_eqn pre)
+    preprocess_functrans thy
+    #> (map o apfst) (rewrite_eqn pre)
   end;
 
 fun preprocess_conv thy ct =