--- a/src/HOL/Library/Efficient_Nat.thy Tue May 12 21:17:34 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue May 12 21:17:38 2009 +0200
@@ -179,7 +179,7 @@
else NONE
end;
-val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
+val eqn_suc_preproc = Code_Preproc.simple_functrans (gen_eqn_suc_preproc
@{thm Suc_if_eq} I (fst o Logic.dest_equals));
fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
@@ -229,7 +229,7 @@
Codegen.add_preprocessor eqn_suc_preproc'
#> Codegen.add_preprocessor clause_suc_preproc
- #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
+ #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
end;
*}