src/Tools/nbe.ML

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