--- 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;
*}
--- 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)
--- 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 =