# HG changeset patch
# User haftmann
# Date 1242155858 -7200
# Node ID b3bb28c8740989c03d65d9c2bca923b32d2c0a04
# Parent  b63c3f6bd3bee5bbbc90a2ae39073d721cbcaf0d
adapted to changes in module Code

diff -r b63c3f6bd3be -r b3bb28c87409 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue May 12 21:17:34 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 12 21:17:38 2009 +0200
@@ -179,7 +179,7 @@
        else NONE
   end;
 
-val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
+val eqn_suc_preproc = Code_Preproc.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
@@ -229,7 +229,7 @@
 
   Codegen.add_preprocessor eqn_suc_preproc'
   #> Codegen.add_preprocessor clause_suc_preproc
-  #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
+  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
 
 end;
 *}