1.1 --- a/src/Tools/nbe.ML	Wed Aug 15 22:21:13 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Aug 16 11:45:05 2007 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4    Logic.mk_equals (t, eval thy code t t' deps);
     1.5  
     1.6  fun normalization_invoke thy code t t' deps =
     1.7 -  Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps));
     1.8 +  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t', deps));
     1.9    (*FIXME get rid of hardwired theory name*)
    1.10  
    1.11  fun normalization_conv ct =