1.1 --- a/src/HOL/HOL.thy	Tue May 12 17:09:36 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 12 19:30:33 2009 +0200
     1.3 @@ -1870,8 +1870,8 @@
     1.4  subsubsection {* Generic code generator preprocessor *}
     1.5  
     1.6  setup {*
     1.7 -  Code.map_pre (K HOL_basic_ss)
     1.8 -  #> Code.map_post (K HOL_basic_ss)
     1.9 +  Code_Preproc.map_pre (K HOL_basic_ss)
    1.10 +  #> Code_Preproc.map_post (K HOL_basic_ss)
    1.11  *}
    1.12  
    1.13  subsubsection {* Generic code generator target languages *}