1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 09:13:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 10:18:45 2010 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4        end
     1.5    in get_first mk_thms eqs end;
     1.6  
     1.7 -fun eqn_suc_preproc thy thms =
     1.8 +fun eqn_suc_base_preproc thy thms =
     1.9    let
    1.10      val dest = fst o Logic.dest_equals o prop_of;
    1.11      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.12 @@ -171,10 +171,7 @@
    1.13         else NONE
    1.14    end;
    1.15  
    1.16 -val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc;
    1.17 -
    1.18 -fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms
    1.19 -  |> the_default thms;
    1.20 +val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
    1.21  
    1.22  fun remove_suc_clause thy thms =
    1.23    let
    1.24 @@ -217,9 +214,8 @@
    1.25    end;
    1.26  in
    1.27  
    1.28 -  Codegen.add_preprocessor eqn_suc_preproc2
    1.29 +  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.30    #> Codegen.add_preprocessor clause_suc_preproc
    1.31 -  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1)
    1.32  
    1.33  end;
    1.34  *}