src/HOL/Library/Efficient_Nat.thy
changeset 31090 3be41b271023
parent 30663 0b6aff7451b2
child 31128 b3bb28c87409
--- 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