src/HOL/Library/Efficient_Nat.thy
changeset 31090 3be41b271023
parent 30663 0b6aff7451b2
child 31128 b3bb28c87409
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon May 11 09:40:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon May 11 10:53:19 2009 +0200
     1.3 @@ -179,10 +179,8 @@
     1.4         else NONE
     1.5    end;
     1.6  
     1.7 -fun eqn_suc_preproc thy = map fst
     1.8 -  #> gen_eqn_suc_preproc
     1.9 -      @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
    1.10 -  #> (Option.map o map) (Code_Unit.mk_eqn thy);
    1.11 +val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
    1.12 +  @{thm Suc_if_eq} I (fst o Logic.dest_equals));
    1.13  
    1.14  fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
    1.15    @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms