--- a/src/HOL/Library/Efficient_Nat.thy Mon May 11 09:40:39 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon May 11 10:53:19 2009 +0200
@@ -179,10 +179,8 @@
else NONE
end;
-fun eqn_suc_preproc thy = map fst
- #> gen_eqn_suc_preproc
- @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
- #> (Option.map o map) (Code_Unit.mk_eqn thy);
+val eqn_suc_preproc = Code.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
@{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms