1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue May 12 21:17:34 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 12 21:17:38 2009 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4         else NONE
     1.5    end;
     1.6  
     1.7 -val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
     1.8 +val eqn_suc_preproc = Code_Preproc.simple_functrans (gen_eqn_suc_preproc
     1.9    @{thm Suc_if_eq} I (fst o Logic.dest_equals));
    1.10  
    1.11  fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
    1.12 @@ -229,7 +229,7 @@
    1.13  
    1.14    Codegen.add_preprocessor eqn_suc_preproc'
    1.15    #> Codegen.add_preprocessor clause_suc_preproc
    1.16 -  #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.17 +  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.18  
    1.19  end;
    1.20  *}